diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations.out | 12 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 6e59c36777..47eafe5537 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -8,17 +8,17 @@ fun e : nat * nat => proj1 e Identifier 'decomp' now a keyword decomp (true, true) as t, u in (t, u) : bool * bool -!(0 = 0) +! (0 = 0) : Prop forall n : nat, n = 0 : Prop -!(0 = 0) +! (0 = 0) : Prop -forall n : nat, #(n = n) +forall n : nat, # (n = n) : Prop -forall n n0 : nat, ##(n = n0) +forall n n0 : nat, ## (n = n0) : Prop -forall n n0 : nat, ###(n = n0) +forall n n0 : nat, ### (n = n0) : Prop 3 + 3 : Z @@ -42,7 +42,7 @@ Identifier 'ifn' now a keyword Identifier 'is' now a keyword fun x : nat => ifn x is succ n then n else 0 : nat -> nat -1- +1 - : bool -4 : Z diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index cf45025ea4..3639c6c3de 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -1,6 +1,6 @@ 2 3 : PAIR -2[+]3 +2 [+] 3 : nat forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x : Prop |