From eec5145a5c6575d04b5ab442597fb52913daed29 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 4 Feb 2017 14:56:04 +0100 Subject: Applying same convention as in Definition for printing type in a let in. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 *) --- test-suite/output/inference.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/output/inference.out') 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] -- cgit v1.2.3