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

feat: expand show-by and have-by macros

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-14 15:08:05 -07:00
parent 8586ec1759
commit a6b19cd4af
2 changed files with 27 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Lean/Elab/BuiltinNotation.lean
View file

@ -55,16 +55,19 @@ fun stx expectedType? => match_syntax stx with
@[builtinMacro Lean.Parser.Term.show] def expandShow : Macro :=
fun stx => match_syntax stx with
| `(show $type from $val) => let thisId := mkIdentFrom stx `this; `(let! $thisId : $type := $val; $thisId)
| _ => Macro.throwUnsupported
| `(show $type from $val) => let thisId := mkIdentFrom stx `this; `(let! $thisId : $type := $val; $thisId)
| `(show $type by $tac:tacticSeq) => `(show $type from by $tac:tacticSeq)
| _ => Macro.throwUnsupported
@[builtinMacro Lean.Parser.Term.have] def expandHave : Macro :=
fun stx => match_syntax stx with
| `(have $type from $val; $body) => let thisId := mkIdentFrom stx `this; `(let! $thisId : $type := $val; $body)
| `(have $type := $val; $body) => let thisId := mkIdentFrom stx `this; `(let! $thisId : $type := $val; $body)
| `(have $x : $type from $val; $body) => `(let! $x:ident : $type := $val; $body)
| `(have $x : $type := $val; $body) => `(let! $x:ident : $type := $val; $body)
| _ => Macro.throwUnsupported
| `(have $type from $val; $body) => let thisId := mkIdentFrom stx `this; `(let! $thisId : $type := $val; $body)
| `(have $type by $tac:tacticSeq; $body) => `(have $type from by $tac:tacticSeq; $body)
| `(have $type := $val; $body) => let thisId := mkIdentFrom stx `this; `(let! $thisId : $type := $val; $body)
| `(have $x : $type from $val; $body) => `(let! $x:ident : $type := $val; $body)
| `(have $x : $type by $tac:tacticSeq; $body) => `(have $x : $type from by $tac:tacticSeq; $body)
| `(have $x : $type := $val; $body) => `(let! $x:ident : $type := $val; $body)
| _ => Macro.throwUnsupported
@[builtinMacro Lean.Parser.Term.where] def expandWhere : Macro :=
fun stx => match_syntax stx with

17
tests/lean/run/newfrontend1.lean
View file

@ -349,3 +349,20 @@ theorem simple21 (x y z : Nat) : y = z → x = x → y = x → x = z :=
fun h1 _ h3 =>
have x = y from by apply Eq.symm; assumption;
Eq.trans this (by assumption)
theorem simple22 (x y z : Nat) : y = z → y = x → id (x = z + 0) :=
fun h1 h2 => show x = z + 0 by
apply Eq.trans;
exact h2.symm;
assumption;
skip
theorem simple23 (x y z : Nat) : y = z → x = x → y = x → x = z :=
fun h1 _ h3 =>
have x = y by apply Eq.symm; assumption;
Eq.trans this (by assumption)
theorem simple24 (x y z : Nat) : y = z → x = x → y = x → x = z :=
fun h1 _ h3 =>
have h : x = y by apply Eq.symm; assumption;
Eq.trans h (by assumption)