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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-13 08:37:34 -07:00
parent 1f4039a25d
commit 3e0a975e9c
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,7 +1,7 @@
example : x ≠ y → x ∉ [y] :=
fun hne hin =>
match hin with
| .head _ => hne rfl
| .head _ _ => hne rfl
example : x ≠ y → x ∉ [y] :=
fun hne (.head _) => hne rfl
fun hne (.head _ _) => hne rfl