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

fix: unclear TSyntax breakage

Browse source
This commit is contained in:
Sebastian Ullrich 2022-06-15 15:48:11 +02:00
parent 86cd656fc6
commit fe22d84143
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Tactics.lean
View file

@ -285,7 +285,7 @@ macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_)
/--
`have h := e` adds the hypothesis `h : t` if `e : t`.
-/
macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
macro (name := «tacticHave__:=_») (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
/--
Given a main goal `ctx |- t`, `suffices h : t' from e` replaces the main goal with `ctx |- t'`,
`e` must have type `t` in the context `ctx, h : t'`.