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

test: add injection notation test

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-29 20:41:33 -07:00
parent 0032578d5b
commit 84de2e4a5b
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/injIssue.lean Normal file
View file

@ -0,0 +1,4 @@
theorem ex1 (n m : Nat) : some n = some m → n = m := by
intro h
injection h with h
exact h