aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations2.out
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-02-04 14:56:04 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 12:22:21 +0100
commiteec5145a5c6575d04b5ab442597fb52913daed29 (patch)
treeefdc1db3c3b4db77cc5d5382b8424794db5f4201 /test-suite/output/Notations2.out
parent6899bace8e617f38fadce0b4b660d951d73af5d0 (diff)
Applying same convention as in Definition for printing type in a let in.
Also adding spaces around ":=" and ":" when printed as "(x : t := c)". Example: Check fun y => let x : True := I in fun z => z+y=0. (* λ (y : nat) (x : True := I) (z : nat), z + y = 0 : nat → nat → Prop *)
Diffstat (limited to 'test-suite/output/Notations2.out')
-rw-r--r--test-suite/output/Notations2.out2
1 files changed, 1 insertions, 1 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