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

test: have-by in tactic mode

Browse source 
@Kha By adding `have-by` macro (in term mode), we got `have-by` in
tactic mode without writing a single line of code :)
This commit is contained in:
Leonardo de Moura 2020-09-14 15:13:07 -07:00
parent a6b19cd4af
commit ca90ff8b59
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
tests/lean/run/tactic1.lean
View file

@ -44,3 +44,18 @@ by {
exact h₁;
exact h₃
}
theorem ex7 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
by {
have y = z by apply Eq.symm; assumption;
apply Eq.trans;
exact h₁;
assumption
}
theorem ex8 (x y z : Nat) (h₁ : x = y) (h₂ : z = y) : x = z :=
by apply Eq.trans h₁;
have y = z by
apply Eq.symm;
assumption;
exact this