max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-15 12:40:45 -07:00
parent f6651605d0
commit 47bb80a277
2 changed files with 332 additions and 333 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
stage0/src/Lean/Elab/Quotation.lean generated
View file

@ -114,8 +114,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
| none => Array.empty)
| _ =>
let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id $arr)) ids.back
let tuple ← mkTuple ids
`(Array.map (fun $tuple => $(inner[0])) $arr)
`(Array.map (fun $(← mkTuple ids) => $(inner[0])) $arr)
let arr ←
if k == `sepBy then
`(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))

662
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

File diff suppressed because it is too large Load diff