Skip to content

Commit 24b858b

Browse files
gebnergebner
committed
Fix test.
1 parent 81798ae commit 24b858b

File tree

3 files changed

+51
-51
lines changed

3 files changed

+51
-51
lines changed

‎tests/error-messages/Monoid.fst.json_output.expected

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -345,8 +345,8 @@ let left_action_morphism f mf la lb = forall (g: ma) (x: a). lb.act (mf g) (f x)
345345
Module after type checking:
346346
module Monoid
347347
Declarations: [
348-
let right_unitality_lemma m u476 mult = forall (x: m). mult x u476 == x
349-
let left_unitality_lemma m u476 mult = forall (x: m). mult u476 x == x
348+
let right_unitality_lemma m u466 mult = forall (x: m). mult x u466 == x
349+
let left_unitality_lemma m u466 mult = forall (x: m). mult u466 x == x
350350
let associativity_lemma m mult = forall (x: m) (y: m) (z: m). mult (mult x y) z == mult x (mult y z)
351351
unopteq
352352
type monoid (m: Type) =
@@ -382,25 +382,25 @@ val monoid__uu___haseq: Prims.l_True /\
382382

383383

384384

385-
let intro_monoid m u476 mult = Monoid.Monoid u476 mult () () () <: Prims.Pure (Monoid.monoid m)
385+
let intro_monoid m u466 mult = Monoid.Monoid u466 mult () () () <: Prims.Pure (Monoid.monoid m)
386386
let nat_plus_monoid =
387387
let add x y = x + y <: Prims.nat in
388388
Monoid.intro_monoid Prims.nat 0 add
389389
let int_plus_monoid = Monoid.intro_monoid Prims.int 0 Prims.op_Addition
390390
let conjunction_monoid =
391-
let u474 = FStar.Pervasives.singleton Prims.l_True in
391+
let u464 = FStar.Pervasives.singleton Prims.l_True in
392392
let mult p q = p /\ q <: Prims.prop in
393393
let left_unitality_helper p =
394-
(assert (mult u474 p <==> p);
395-
FStar.PropositionalExtensionality.apply (mult u474 p) p)
394+
(assert (mult u464 p <==> p);
395+
FStar.PropositionalExtensionality.apply (mult u464 p) p)
396396
<:
397-
FStar.Pervasives.Lemma (ensures mult u474 p == p)
397+
FStar.Pervasives.Lemma (ensures mult u464 p == p)
398398
in
399399
let right_unitality_helper p =
400-
(assert (mult p u474 <==> p);
401-
FStar.PropositionalExtensionality.apply (mult p u474) p)
400+
(assert (mult p u464 <==> p);
401+
FStar.PropositionalExtensionality.apply (mult p u464) p)
402402
<:
403-
FStar.Pervasives.Lemma (ensures mult p u474 == p)
403+
FStar.Pervasives.Lemma (ensures mult p u464 == p)
404404
in
405405
let associativity_helper p1 p2 p3 =
406406
(assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3));
@@ -409,26 +409,26 @@ let conjunction_monoid =
409409
FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3))
410410
in
411411
FStar.Classical.forall_intro right_unitality_helper;
412-
assert (Monoid.right_unitality_lemma Prims.prop u474 mult);
412+
assert (Monoid.right_unitality_lemma Prims.prop u464 mult);
413413
FStar.Classical.forall_intro left_unitality_helper;
414-
assert (Monoid.left_unitality_lemma Prims.prop u474 mult);
414+
assert (Monoid.left_unitality_lemma Prims.prop u464 mult);
415415
FStar.Classical.forall_intro_3 associativity_helper;
416416
assert (Monoid.associativity_lemma Prims.prop mult);
417-
Monoid.intro_monoid Prims.prop u474 mult
417+
Monoid.intro_monoid Prims.prop u464 mult
418418
let disjunction_monoid =
419-
let u474 = FStar.Pervasives.singleton Prims.l_False in
419+
let u464 = FStar.Pervasives.singleton Prims.l_False in
420420
let mult p q = p \/ q <: Prims.prop in
421421
let left_unitality_helper p =
422-
(assert (mult u474 p <==> p);
423-
FStar.PropositionalExtensionality.apply (mult u474 p) p)
422+
(assert (mult u464 p <==> p);
423+
FStar.PropositionalExtensionality.apply (mult u464 p) p)
424424
<:
425-
FStar.Pervasives.Lemma (ensures mult u474 p == p)
425+
FStar.Pervasives.Lemma (ensures mult u464 p == p)
426426
in
427427
let right_unitality_helper p =
428-
(assert (mult p u474 <==> p);
429-
FStar.PropositionalExtensionality.apply (mult p u474) p)
428+
(assert (mult p u464 <==> p);
429+
FStar.PropositionalExtensionality.apply (mult p u464) p)
430430
<:
431-
FStar.Pervasives.Lemma (ensures mult p u474 == p)
431+
FStar.Pervasives.Lemma (ensures mult p u464 == p)
432432
in
433433
let associativity_helper p1 p2 p3 =
434434
(assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3));
@@ -437,12 +437,12 @@ let disjunction_monoid =
437437
FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3))
438438
in
439439
FStar.Classical.forall_intro right_unitality_helper;
440-
assert (Monoid.right_unitality_lemma Prims.prop u474 mult);
440+
assert (Monoid.right_unitality_lemma Prims.prop u464 mult);
441441
FStar.Classical.forall_intro left_unitality_helper;
442-
assert (Monoid.left_unitality_lemma Prims.prop u474 mult);
442+
assert (Monoid.left_unitality_lemma Prims.prop u464 mult);
443443
FStar.Classical.forall_intro_3 associativity_helper;
444444
assert (Monoid.associativity_lemma Prims.prop mult);
445-
Monoid.intro_monoid Prims.prop u474 mult
445+
Monoid.intro_monoid Prims.prop u464 mult
446446
let bool_and_monoid =
447447
let and_ b1 b2 = b1 && b2 in
448448
Monoid.intro_monoid Prims.bool true and_
@@ -520,7 +520,7 @@ let _ =
520520
Monoid.intro_monoid_morphism Monoid.neg Monoid.disjunction_monoid Monoid.conjunction_monoid
521521
let mult_act_lemma m a mult act =
522522
forall (x: m) (x': m) (y: a). act (mult x x') y == act x (act x' y)
523-
let unit_act_lemma m a u478 act = forall (y: a). act u478 y == y
523+
let unit_act_lemma m a u468 act = forall (y: a). act u468 y == y
524524
unopteq
525525
type left_action (mm: Monoid.monoid m) (a: Type) =
526526
| LAct :

‎tests/error-messages/Monoid.fst.output.expected

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -345,8 +345,8 @@ let left_action_morphism f mf la lb = forall (g: ma) (x: a). lb.act (mf g) (f x)
345345
Module after type checking:
346346
module Monoid
347347
Declarations: [
348-
let right_unitality_lemma m u476 mult = forall (x: m). mult x u476 == x
349-
let left_unitality_lemma m u476 mult = forall (x: m). mult u476 x == x
348+
let right_unitality_lemma m u466 mult = forall (x: m). mult x u466 == x
349+
let left_unitality_lemma m u466 mult = forall (x: m). mult u466 x == x
350350
let associativity_lemma m mult = forall (x: m) (y: m) (z: m). mult (mult x y) z == mult x (mult y z)
351351
unopteq
352352
type monoid (m: Type) =
@@ -382,25 +382,25 @@ val monoid__uu___haseq: Prims.l_True /\
382382

383383

384384

385-
let intro_monoid m u476 mult = Monoid.Monoid u476 mult () () () <: Prims.Pure (Monoid.monoid m)
385+
let intro_monoid m u466 mult = Monoid.Monoid u466 mult () () () <: Prims.Pure (Monoid.monoid m)
386386
let nat_plus_monoid =
387387
let add x y = x + y <: Prims.nat in
388388
Monoid.intro_monoid Prims.nat 0 add
389389
let int_plus_monoid = Monoid.intro_monoid Prims.int 0 Prims.op_Addition
390390
let conjunction_monoid =
391-
let u474 = FStar.Pervasives.singleton Prims.l_True in
391+
let u464 = FStar.Pervasives.singleton Prims.l_True in
392392
let mult p q = p /\ q <: Prims.prop in
393393
let left_unitality_helper p =
394-
(assert (mult u474 p <==> p);
395-
FStar.PropositionalExtensionality.apply (mult u474 p) p)
394+
(assert (mult u464 p <==> p);
395+
FStar.PropositionalExtensionality.apply (mult u464 p) p)
396396
<:
397-
FStar.Pervasives.Lemma (ensures mult u474 p == p)
397+
FStar.Pervasives.Lemma (ensures mult u464 p == p)
398398
in
399399
let right_unitality_helper p =
400-
(assert (mult p u474 <==> p);
401-
FStar.PropositionalExtensionality.apply (mult p u474) p)
400+
(assert (mult p u464 <==> p);
401+
FStar.PropositionalExtensionality.apply (mult p u464) p)
402402
<:
403-
FStar.Pervasives.Lemma (ensures mult p u474 == p)
403+
FStar.Pervasives.Lemma (ensures mult p u464 == p)
404404
in
405405
let associativity_helper p1 p2 p3 =
406406
(assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3));
@@ -409,26 +409,26 @@ let conjunction_monoid =
409409
FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3))
410410
in
411411
FStar.Classical.forall_intro right_unitality_helper;
412-
assert (Monoid.right_unitality_lemma Prims.prop u474 mult);
412+
assert (Monoid.right_unitality_lemma Prims.prop u464 mult);
413413
FStar.Classical.forall_intro left_unitality_helper;
414-
assert (Monoid.left_unitality_lemma Prims.prop u474 mult);
414+
assert (Monoid.left_unitality_lemma Prims.prop u464 mult);
415415
FStar.Classical.forall_intro_3 associativity_helper;
416416
assert (Monoid.associativity_lemma Prims.prop mult);
417-
Monoid.intro_monoid Prims.prop u474 mult
417+
Monoid.intro_monoid Prims.prop u464 mult
418418
let disjunction_monoid =
419-
let u474 = FStar.Pervasives.singleton Prims.l_False in
419+
let u464 = FStar.Pervasives.singleton Prims.l_False in
420420
let mult p q = p \/ q <: Prims.prop in
421421
let left_unitality_helper p =
422-
(assert (mult u474 p <==> p);
423-
FStar.PropositionalExtensionality.apply (mult u474 p) p)
422+
(assert (mult u464 p <==> p);
423+
FStar.PropositionalExtensionality.apply (mult u464 p) p)
424424
<:
425-
FStar.Pervasives.Lemma (ensures mult u474 p == p)
425+
FStar.Pervasives.Lemma (ensures mult u464 p == p)
426426
in
427427
let right_unitality_helper p =
428-
(assert (mult p u474 <==> p);
429-
FStar.PropositionalExtensionality.apply (mult p u474) p)
428+
(assert (mult p u464 <==> p);
429+
FStar.PropositionalExtensionality.apply (mult p u464) p)
430430
<:
431-
FStar.Pervasives.Lemma (ensures mult p u474 == p)
431+
FStar.Pervasives.Lemma (ensures mult p u464 == p)
432432
in
433433
let associativity_helper p1 p2 p3 =
434434
(assert (mult (mult p1 p2) p3 <==> mult p1 (mult p2 p3));
@@ -437,12 +437,12 @@ let disjunction_monoid =
437437
FStar.Pervasives.Lemma (ensures mult (mult p1 p2) p3 == mult p1 (mult p2 p3))
438438
in
439439
FStar.Classical.forall_intro right_unitality_helper;
440-
assert (Monoid.right_unitality_lemma Prims.prop u474 mult);
440+
assert (Monoid.right_unitality_lemma Prims.prop u464 mult);
441441
FStar.Classical.forall_intro left_unitality_helper;
442-
assert (Monoid.left_unitality_lemma Prims.prop u474 mult);
442+
assert (Monoid.left_unitality_lemma Prims.prop u464 mult);
443443
FStar.Classical.forall_intro_3 associativity_helper;
444444
assert (Monoid.associativity_lemma Prims.prop mult);
445-
Monoid.intro_monoid Prims.prop u474 mult
445+
Monoid.intro_monoid Prims.prop u464 mult
446446
let bool_and_monoid =
447447
let and_ b1 b2 = b1 && b2 in
448448
Monoid.intro_monoid Prims.bool true and_
@@ -520,7 +520,7 @@ let _ =
520520
Monoid.intro_monoid_morphism Monoid.neg Monoid.disjunction_monoid Monoid.conjunction_monoid
521521
let mult_act_lemma m a mult act =
522522
forall (x: m) (x': m) (y: a). act (mult x x') y == act x (act x' y)
523-
let unit_act_lemma m a u478 act = forall (y: a). act u478 y == y
523+
let unit_act_lemma m a u468 act = forall (y: a). act u468 y == y
524524
unopteq
525525
type left_action (mm: Monoid.monoid m) (a: Type) =
526526
| LAct :

‎tests/tactics/Postprocess.fst.output.expected

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -482,11 +482,11 @@ in
482482
[@ ]
483483
visible let apply_feq_lem : ($f:(uu___:a@1:(Tm_unknown) -> Tot b@1:(Tm_unknown)) -> $g:(uu___:a@2:(Tm_unknown) -> Tot b@2:(Tm_unknown)) -> Lemma (unit)) = (fun $f $g -> (congruence_fun f@1:(Tm_unknown) g@0:(Tm_unknown) ()))
484484
[@ ]
485-
visible let fext : (uu___:unit -> Tac (unit)) = (fun uu___ -> let uu___#1096 : unit = (apply_lemma `(apply_feq_lem)[])
485+
visible let fext : (uu___:unit -> Tac (unit)) = (fun uu___ -> let uu___#1098 : unit = (apply_lemma `(apply_feq_lem)[])
486486
in
487-
let uu___#1097 : unit = (dismiss ())
487+
let uu___#1099 : unit = (dismiss ())
488488
in
489-
let uu___#1098 : (list binding) = (forall_intros ())
489+
let uu___#1100 : (list binding) = (forall_intros ())
490490
in
491491
(ignore uu___@0:(Tm_unknown)))
492492
[@ ]

0 commit comments

Comments
 (0)