diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
| -rw-r--r-- | test-suite/output/inference.out | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index ad60aeccc..1ec701ae8 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -32,7 +32,7 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d : Type -> Prop λ A : Type, ∀ n p : A, n = p : Type -> Prop -let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 +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) : (nat -> nat) -> nat -> nat diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index 576fbd7c0..e83e7176d 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,7 +6,7 @@ fun e : option L => match e with : option L -> option L 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 : T n in ?y ?y0 : T n +fun n : nat => let x : T n := A n in ?y ?y0 : T n : forall n : nat, T n where ?y : [n : nat x := A n : T n |- ?T -> T n] |