diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-04 14:56:04 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 12:22:21 +0100 |
| commit | eec5145a5c6575d04b5ab442597fb52913daed29 (patch) | |
| tree | efdc1db3c3b4db77cc5d5382b8424794db5f4201 | |
| parent | 6899bace8e617f38fadce0b4b660d951d73af5d0 (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 *)
| -rw-r--r-- | printing/ppconstr.ml | 11 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
| -rw-r--r-- | test-suite/output/inference.out | 2 |
3 files changed, 8 insertions, 7 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 0013d49a1..f36c8c153 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -363,8 +363,9 @@ let tag_var = tag Tag.variable | CLocalAssum (nal,k,t) -> pr_binder true pr_c (nal,k,t) | CLocalDef (na,c,topt) -> - surround (pr_lname na ++ str":=" ++ cut() ++ pr_c c ++ - pr_opt_no_spc (fun t -> cut () ++ str ":" ++ pr_c t) topt) + surround (pr_lname na ++ + pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++ + str" :=" ++ spc() ++ pr_c c) | CLocalPattern (loc,p,tyo) -> let p = pr_patt lsimplepatt p in match tyo with @@ -598,9 +599,9 @@ let tag_var = tag Tag.variable | CLetIn (_,x,a,t,b) -> return ( hv 0 ( - hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :=" - ++ pr spc ltop a ++ spc () - ++ pr_opt_no_spc (fun t -> str ":" ++ ws 1 ++ pr mt ltop t ++ spc ()) t + hov 2 (keyword "let" ++ spc () ++ pr_lname x + ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr mt ltop t) t + ++ str " :=" ++ pr spc ltop a ++ spc () ++ keyword "in") ++ pr spc ltop b), lletin 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] |