diff options
| -rw-r--r-- | test-suite/output/Notations.out | 13 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
| -rw-r--r-- | test-suite/output/inference.out | 6 |
3 files changed, 9 insertions, 12 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index d81a71e4ac..0bf922f647 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -2,10 +2,8 @@ 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) @@ -28,18 +26,14 @@ 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 - @@ -78,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|] @@ -123,14 +116,14 @@ fun x : list ?T0 => match x with | (_ :') t => SOME2 t end : list ?T0 -> option (list ?T0) -s +where +?T0 : [x : list ?T0 |- Type] (x 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 diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 958001c39f..58ec1de563 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -24,7 +24,6 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d : Prop ∀ n p : nat, n + p = 0 : Prop -Identifier 'λ' now a keyword λ n p : nat, n + p = 0 : nat -> nat -> Prop λ (A : Type) (n p : A), n = p @@ -33,7 +32,6 @@ Identifier 'λ' now a keyword : Type -> Prop λ A : Type, ∀ n p : A, n = p : Type -> Prop -Identifier 'let'' now a keyword let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 : bool -> nat λ (f : nat -> nat) (x : nat), f(x) + S(x) diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index 6701259760..d69baaece5 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -10,5 +10,11 @@ fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p fun n : nat => let x := A n in ?y ?y0:T n : forall n : nat, T n +where +?y : [n : nat x := A n : T n |- ?T0 -> T n] +?y0 : [n : nat x := A n : T n |- ?T0] fun n : nat => ?y ?y0:T n : forall n : nat, T n +where +?y : [n : nat |- ?T0 -> T n] +?y0 : [n : nat |- ?T0] |