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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-13 18:31:50 -08:00
parent bfc1a16c02
commit 6e3792e995
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -14,7 +14,7 @@ class HasCoerce (a b : Type) :=
def coerce {a b : Type} [HasCoerce a b] : a → b :=
@HasCoerce.coerce a b _
instance coerceTrans {a b c : Type} [HasCoerce b c] [HasCoerce a b] : HasCoerce a c :=
instance coerceTrans {a b c : Type} [HasCoerce a b] [HasCoerce b c] : HasCoerce a c :=
⟨fun x => coerce (coerce x : b)⟩
instance coerceBoolToProp : HasCoerce Bool Prop :=

2
tests/lean/sanitychecks.lean.expected.out
View file

@ -1,4 +1,4 @@
sanitychecks.lean:1:0: error: fail to show termination for
sanitychecks.lean:1:8: error: fail to show termination for
unsound
with errors
structural recursion cannot be used