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 2020-11-19 08:28:52 -08:00
parent a58a7d6536
commit 998dd05c65
2 changed files with 1594 additions and 1470 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/Lean/Elab/App.lean generated
View file

@ -735,6 +735,9 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
| `($e $.$field) => do
let f ← `($(e).$field)
elabAppFn f lvals namedArgs args expectedType? explicit ellipsis overloaded acc
| `($e |>. $field) => do
let f ← `($(e).$field)
elabAppFn f lvals namedArgs args expectedType? explicit ellipsis overloaded acc
| `($(e).$field:ident) =>
let newLVals := field.getId.eraseMacroScopes.components.map (fun n => LVal.fieldName (toString n))
elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
@ -855,6 +858,7 @@ private def elabAtom : TermElab := fun stx expectedType? =>
@[builtinTermElab namedPattern] def elabNamedPattern : TermElab := elabAtom
@[builtinTermElab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
@[builtinTermElab dollarProj] def expandDollarProj : TermElab := elabAtom
@[builtinTermElab pipeProj] def expandPipeProj : TermElab := elabAtom
@[builtinTermElab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
match_syntax stx with

3060
stage0/stdlib/Lean/Elab/App.c generated
View file

File diff suppressed because it is too large Load diff