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 2024-06-19 15:49:33 -07:00 • committed by Leonardo de Moura
parent 53be53f5ae
commit 3e05b0641b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/constructor_as_variable.lean
View file

@ -97,7 +97,7 @@ Suggestions:
'Array.Mem.mk',
'Array.mk',
'BEq.mk',
(or 199 others)
(or 200 others)
-/
#guard_msgs in
def ctorSuggestion1 (pair : α × β) : β :=