diff options
Diffstat (limited to 'test-suite/output/Notations.out')
| -rw-r--r-- | test-suite/output/Notations.out | 45 |
1 files changed, 21 insertions, 24 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 66307236..60ee72b3 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -2,23 +2,21 @@ true ? 0; 1 : nat if true as x return (x ? nat; bool) then 0 else true : nat -Identifier 'proj1' now a keyword fun e : nat * nat => proj1 e : nat * nat -> nat -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 @@ -28,21 +26,17 @@ forall n n0 : nat, ###(n = n0) : list nat (1; 2, 4) : nat * nat * nat -Identifier 'ifzero' now a keyword ifzero 3 : bool -Identifier 'pred' now a keyword pred 3 : nat fun n : nat => pred n : nat -> nat fun n : nat => pred n : nat -> nat -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 @@ -50,14 +44,12 @@ The command has indeed failed with message: => Error: x should not be bound in a recursive pattern of the right-hand side. The command has indeed failed with message: => Error: in the right-hand side, y and z should appear in - term position as part of a recursive pattern. +term position as part of a recursive pattern. The command has indeed failed with message: => Error: The reference w was not found in the current environment. The command has indeed failed with message: -=> Error: x is unbound in the right-hand side. -The command has indeed failed with message: => Error: in the right-hand side, y and z should appear in - term position as part of a recursive pattern. +term position as part of a recursive pattern. The command has indeed failed with message: => Error: z is expected to occur in binding position in the right-hand side. The command has indeed failed with message: @@ -80,7 +72,6 @@ Nil : forall A : Type, list A NIL:list nat : list nat -Identifier 'I' now a keyword (false && I 3)%bool /\ I 6 : Prop [|1, 2, 3; 4, 5, 6|] @@ -89,11 +80,11 @@ Identifier 'I' now a keyword : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool)) fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z : (Z -> Z -> Z -> Z) -> Z -plus +Init.Nat.add : nat -> nat -> nat S : nat -> nat -mult +Init.Nat.mul : nat -> nat -> nat le : nat -> nat -> Prop @@ -101,7 +92,7 @@ plus : nat -> nat -> nat succ : nat -> nat -mult +Init.Nat.mul : nat -> nat -> nat le : nat -> nat -> Prop @@ -116,18 +107,24 @@ fun x : option Z => match x with end : option Z -> Z fun x : option Z => match x with - | SOME3 x0 => x0 - | NONE3 => 0 + | SOME2 x0 => x0 + | NONE2 => 0 end : option Z -> Z +fun x : list ?T1 => match x with + | NIL => NONE2 + | (_ :') t => SOME2 t + end + : list ?T1 -> option (list ?T1) +where +?T1 : [x : list ?T1 x1 : list ?T1 x0 := x1 : list ?T1 |- Type] (x, x1, + x0 cannot be used) s : s -Identifier 'foo' now a keyword 10 : nat fun _ : nat => 9 : nat -> nat -Identifier 'ONE' now a keyword fun (x : nat) (p : x = x) => match p with | ONE => ONE end = p |