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

feat: elaborate have

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-02 14:16:20 -08:00
parent 04a0907954
commit 16aff9a182
2 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Lean/Elab/BuiltinNotation.lean
View file

@ -60,6 +60,14 @@ adaptExpander $ fun stx => match_syntax stx with
| `(show $type from $val) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $thisId) $val)
| _ => throwUnexpectedSyntax stx "show-from"
@[builtinTermElab «have»] def elabHave : TermElab :=
adaptExpander $ fun stx => match_syntax stx with
| `(have $type from $val; $body) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $body) $val)
| `(have $type := $val; $body) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $body) $val)
| `(have $x : $type from $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
| `(have $x : $type := $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
| _ => throwUnexpectedSyntax stx "have"
def elabInfix (f : Syntax) : TermElab :=
fun stx expectedType? => do
-- term `op` term

4
tests/lean/run/frontend1.lean
View file

@ -187,3 +187,7 @@ f a
#eval run "#check let x := ⟨1, 2⟩; Prod.fst x"
#eval run "#check show Nat from 1"
#eval run "#check show Int from 1"
#eval run "#check have Nat from one + zero; this + this"
#eval run "#check have x : Nat from one + zero; x + x"
#eval run "#check have Nat := one + zero; this + this"
#eval run "#check have x : Nat := one + zero; x + x"