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

fix: tests

Browse source
This commit is contained in:
Gabriel Ebner 2023-04-11 17:18:52 -07:00 • committed by Leonardo de Moura
parent 8de8c80119
commit 41729263c5
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tests/lean/substBadMotive.lean.expected.out
View file

@ -1,4 +1,5 @@
substBadMotive.lean:7:4-7:16: warning: declaration uses 'sorry'
substBadMotive.lean:9:23-9:44: error: invalid `▸` notation, failed to compute motive for the substitution
substBadMotive.lean:15:22-15:43: error: invalid `▸` notation, failed to compute motive for the substitution
substBadMotive.lean:13:0-17:24: error: well-founded recursion cannot be used, 'Ex3.heapifyDown' does not take any (non-fixed) arguments
substBadMotive.lean:34:30-34:53: error: invalid `▸` notation, failed to compute motive for the substitution