Update example

FStarLang · Nov 14, 2023 · 78e4d9f · 78e4d9f
1 parent a9589a5
commit 78e4d9f
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/examples/typeclasses/Inlining.fst b/examples/typeclasses/Inlining.fst
@@ -39,8 +39,11 @@ let elem' #a {|d : inhab a|} =
 [@@ tcnorm]
 instance inhab_unit : inhab unit = { elem = fun () -> admit #unit () }
 
-(* This will only succeed if the found instance is inlined, sa
+(* This will only succeed if the found instance is inlined, as
  * can be seen from the failure if one uses --tcnorm false *)
+(* This now fails, since we don't unfold methods between phases, so the
+ * verification happens over the interface and not the definitions. *)
+[@@expect_failure]
 let f (u:unit) =
   let t = elem' #unit () in
   assert (forall y. y == 1)