Diff failed for files /tests/error-messages/_output/Monoid.fst.json_output and /tests/error-messages/Monoid.fst.json_output.expected: --- _output/Monoid.fst.json_output 2025-01-11 21:41:26.835485997 +0000 +++ Monoid.fst.json_output.expected 2025-01-11 21:38:17.331678491 +0000 @@ -345,8 +345,8 @@ Module after type checking: module Monoid Declarations: [ -let right_unitality_lemma m u496 mult = forall (x: m). mult x u496 == x -let left_unitality_lemma m u496 mult = forall (x: m). mult u496 x == x +let right_unitality_lemma m u466 mult = forall (x: m). mult x u466 == x +let left_unitality_lemma m u466 mult = forall (x: m). mult u466 x == x let associativity_lemma m mult = forall (x: m) (y: m) (z: m). mult (mult x y) z == mult x (mult y z) unopteq type monoid (m: Type) = @@ -382,25 +382,25 @@ -let intro_monoid m u496 mult = Monoid.Monoid u496 mult () () () <: Prims.Pure (Monoid.monoid m) +let intro_monoid m u466 mult = Monoid.Monoid u466 mult () () () <: Prims.Pure (Monoid.monoid m) let nat_plus_monoid = let add x y = x + y <: Prims.nat in Monoid.intro_monoid Prims.nat 0 add let int_plus_monoid = Monoid.intro_monoid Prims.int 0 Prims.op_Addition let conjunction_monoid = - let u494 = FStar.Pervasives.singleton Prims.l_True in + let u464 = FStar.Pervasives.singleton Prims.l_True in let mult p q = p /\ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u494 p <==> p); - FStar.PropositionalExtensionality.apply (mult u494 p) p) + (assert (mult u464 p <==> p); + FStar.PropositionalExtensionality.apply (mult u464 p) p) <: - FStar.Pervasives.Lemma (ensures mult u494 p == p) + FStar.Pervasives.Lemma (ensures mult u464 p == p) in let right_unitality_helper p = - (assert (mult p u494 <==> p); - FStar.PropositionalExtensionality.apply (mult p u494) p) + (assert (mult p u464 <==> p); + FStar.PropositionalExtensionality.apply (mult p u464) p) <: - FStar.Pervasives.Lemma (ensures mult p u494 == p) + FStar.Pervasives.Lemma (ensures mult p u464 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -409,26 +409,26 @@ FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u494 mult); + assert (Monoid.right_unitality_lemma Prims.prop u464 mult); FStar.Classical.forall_intro left_unitality_helper; - assert (Monoid.left_unitality_lemma Prims.prop u494 mult); + assert (Monoid.left_unitality_lemma Prims.prop u464 mult); FStar.Classical.forall_intro_3 associativity_helper; assert (Monoid.associativity_lemma Prims.prop mult); - Monoid.intro_monoid Prims.prop u494 mult + Monoid.intro_monoid Prims.prop u464 mult let disjunction_monoid = - let u494 = FStar.Pervasives.singleton Prims.l_False in + let u464 = FStar.Pervasives.singleton Prims.l_False in let mult p q = p \/ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u494 p <==> p); - FStar.PropositionalExtensionality.apply (mult u494 p) p) + (assert (mult u464 p <==> p); + FStar.PropositionalExtensionality.apply (mult u464 p) p) <: - FStar.Pervasives.Lemma (ensures mult u494 p == p) + FStar.Pervasives.Lemma (ensures mult u464 p == p) in let right_unitality_helper p = - (assert (mult p u494 <==> p); - FStar.PropositionalExtensionality.apply (mult p u494) p) + (assert (mult p u464 <==> p); + FStar.PropositionalExtensionality.apply (mult p u464) p) <: - FStar.Pervasives.Lemma (ensures mult p u494 == p) + FStar.Pervasives.Lemma (ensures mult p u464 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -437,12 +437,12 @@ FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u494 mult); + assert (Monoid.rig

Diff failed for files /tests/error-messages/_output/Monoid.fst.output and /tests/error-messages/Monoid.fst.output.expected: --- _output/Monoid.fst.output 2025-01-11 21:41:27.947484809 +0000 +++ Monoid.fst.output.expected 2025-01-11 21:38:17.331678491 +0000 @@ -345,8 +345,8 @@ Module after type checking: module Monoid Declarations: [ -let right_unitality_lemma m u496 mult = forall (x: m). mult x u496 == x -let left_unitality_lemma m u496 mult = forall (x: m). mult u496 x == x +let right_unitality_lemma m u466 mult = forall (x: m). mult x u466 == x +let left_unitality_lemma m u466 mult = forall (x: m). mult u466 x == x let associativity_lemma m mult = forall (x: m) (y: m) (z: m). mult (mult x y) z == mult x (mult y z) unopteq type monoid (m: Type) = @@ -382,25 +382,25 @@ -let intro_monoid m u496 mult = Monoid.Monoid u496 mult () () () <: Prims.Pure (Monoid.monoid m) +let intro_monoid m u466 mult = Monoid.Monoid u466 mult () () () <: Prims.Pure (Monoid.monoid m) let nat_plus_monoid = let add x y = x + y <: Prims.nat in Monoid.intro_monoid Prims.nat 0 add let int_plus_monoid = Monoid.intro_monoid Prims.int 0 Prims.op_Addition let conjunction_monoid = - let u494 = FStar.Pervasives.singleton Prims.l_True in + let u464 = FStar.Pervasives.singleton Prims.l_True in let mult p q = p /\ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u494 p <==> p); - FStar.PropositionalExtensionality.apply (mult u494 p) p) + (assert (mult u464 p <==> p); + FStar.PropositionalExtensionality.apply (mult u464 p) p) <: - FStar.Pervasives.Lemma (ensures mult u494 p == p) + FStar.Pervasives.Lemma (ensures mult u464 p == p) in let right_unitality_helper p = - (assert (mult p u494 <==> p); - FStar.PropositionalExtensionality.apply (mult p u494) p) + (assert (mult p u464 <==> p); + FStar.PropositionalExtensionality.apply (mult p u464) p) <: - FStar.Pervasives.Lemma (ensures mult p u494 == p) + FStar.Pervasives.Lemma (ensures mult p u464 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -409,26 +409,26 @@ FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u494 mult); + assert (Monoid.right_unitality_lemma Prims.prop u464 mult); FStar.Classical.forall_intro left_unitality_helper; - assert (Monoid.left_unitality_lemma Prims.prop u494 mult); + assert (Monoid.left_unitality_lemma Prims.prop u464 mult); FStar.Classical.forall_intro_3 associativity_helper; assert (Monoid.associativity_lemma Prims.prop mult); - Monoid.intro_monoid Prims.prop u494 mult + Monoid.intro_monoid Prims.prop u464 mult let disjunction_monoid = - let u494 = FStar.Pervasives.singleton Prims.l_False in + let u464 = FStar.Pervasives.singleton Prims.l_False in let mult p q = p \/ q <: Prims.prop in let left_unitality_helper p = - (assert (mult u494 p <==> p); - FStar.PropositionalExtensionality.apply (mult u494 p) p) + (assert (mult u464 p <==> p); + FStar.PropositionalExtensionality.apply (mult u464 p) p) <: - FStar.Pervasives.Lemma (ensures mult u494 p == p) + FStar.Pervasives.Lemma (ensures mult u464 p == p) in let right_unitality_helper p = - (assert (mult p u494 <==> p); - FStar.PropositionalExtensionality.apply (mult p u494) p) + (assert (mult p u464 <==> p); + FStar.PropositionalExtensionality.apply (mult p u464) p) <: - FStar.Pervasives.Lemma (ensures mult p u494 == p) + FStar.Pervasives.Lemma (ensures mult p u464 == p) in let associativity_helper p1 p2 p3 = (assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3)); @@ -437,12 +437,12 @@ FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3)) in FStar.Classical.forall_intro right_unitality_helper; - assert (Monoid.right_unitality_lemma Prims.prop u494 mult); + assert (Monoid.right_unitality_lemma P

Diff failed for files /tests/error-messages/_output/NegativeTests.Neg.fst.json_output and /tests/error-messages/NegativeTests.Neg.fst.json_output.expected: --- _output/NegativeTests.Neg.fst.json_output 2025-01-11 21:41:32.139480330 +0000 +++ NegativeTests.Neg.fst.json_output.expected 2025-01-11 21:38:17.335678487 +0000 @@ -20,7 +20,7 @@ {"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.Native.option 'a {Some? _}\ngot type FStar.Pervasives.Native.option 'a","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.Native.fst","start_pos":{"line":33,"col":4},"end_pos":{"line":33,"col":8}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":46,"col":30},"end_pos":{"line":46,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let bad_projector`","While typechecking the top-level declaration `[@@expect_failure] let bad_projector`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":523,"col":4},"end_pos":{"line":523,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]} +{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":520,"col":4},"end_pos":{"line":520,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]} >>] >> Got issues: [ {"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":55,"col":25},"end_pos":{"line":55,"col":26}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let h1`","While typechecking the top-level declaration `[@@expect_failure] let h1`"]}

Diff failed for files /tests/error-messages/_output/NegativeTests.Neg.fst.output and /tests/error-messages/NegativeTests.Neg.fst.output.expected: --- _output/NegativeTests.Neg.fst.output 2025-01-11 21:41:32.599479837 +0000 +++ NegativeTests.Neg.fst.output.expected 2025-01-11 21:38:17.335678487 +0000 @@ -63,7 +63,7 @@ got type FStar.Pervasives.result Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also FStar.Pervasives.fsti(523,4-523,5) + - See also FStar.Pervasives.fsti(520,4-520,5) >>] >> Got issues: [

Process completed with exit code 2.