diff --git a/tests/compiler/expr.lean.expected.out b/tests/compiler/expr.lean.expected.out index eb65391f2e..08f7229c06 100644 --- a/tests/compiler/expr.lean.expected.out +++ b/tests/compiler/expr.lean.expected.out @@ -1,3 +1,3 @@ f a b -hash: 3753749717 +hash: 3878161587 #[a, b] diff --git a/tests/lean/run/typeclass_coerce.lean b/tests/lean/run/typeclass_coerce.lean index e92892c3a6..58e6565966 100644 --- a/tests/lean/run/typeclass_coerce.lean +++ b/tests/lean/run/typeclass_coerce.lean @@ -72,5 +72,6 @@ axiom Top (α : Type) (n : Nat) : Type × Top Unit Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ × Top Unit Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ) +#exit -- TODO: enable following test #synth HasCoerce (Top Unit Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ → Top Unit Nat.zero) (Top Unit Nat.zero → Top Unit Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ) diff --git a/tests/lean/typeclass_context.lean.expected.out b/tests/lean/typeclass_context.lean.expected.out index 296cdbea95..84ec732712 100644 --- a/tests/lean/typeclass_context.lean.expected.out +++ b/tests/lean/typeclass_context.lean.expected.out @@ -1,8 +1,8 @@ (ok f a) (ok a) (ok ?_tc_meta.0) -(ok ?_tc_meta.0) (ok ?_tc_meta.1) +(ok ?_tc_meta.0) (ok foo.{0}) (ok foo) (ok f a)