fix(frontends/lean/pp): pretty printing 'binder'

This commit also replaces many occurrences of 'binders' with 'binder'.

library/data/finset/comb.lean

@@ -125,7 +125,7 @@ quot.lift_on s
     (list.nodup_filter p (subtype.has_property l)))
   (λ l₁ l₂ u, quot.sound (perm.perm_filter u))
 
-notation `{` binders ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
+notation `{` binder ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
 
 theorem filter_empty : filter p ∅ = ∅ := rfl
 

library/data/set/basic.lean

@@ -172,11 +172,11 @@ setext (take x, !or.right_distrib)
 
 -- {x : X | P}
 definition set_of (P : X → Prop) : set X := P
-notation `{` binders `|` r:(scoped:1 P, set_of P) `}` := r
+notation `{` binder `|` r:(scoped:1 P, set_of P) `}` := r
 
 -- {x ∈ s | P}
 definition filter (P : X → Prop) (s : set X) : set X := λx, x ∈ s ∧ P x
-notation `{` binders ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
+notation `{` binder ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
 
 -- '{x, y, z}
 definition insert (x : X) (a : set X) : set X := {y : X | y = x ∨ y ∈ a}

library/data/subtype.lean

@@ -10,7 +10,7 @@ set_option structure.proj_mk_thm true
 structure subtype {A : Type} (P : A → Prop) :=
 tag :: (elt_of : A) (has_property : P elt_of)
 
-notation `{` binders `|` r:(scoped:1 P, subtype P) `}` := r
+notation `{` binder `|` r:(scoped:1 P, subtype P) `}` := r
 
 definition ex_of_sub {A : Type} {P : A → Prop} : { x | P x } → ∃ x, P x
 | (subtype.tag a h) := exists.intro a h

src/frontends/lean/pp.cpp

@@ -648,6 +648,19 @@ auto pretty_fn::pp_app(expr const & e) -> result {
     return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));
 }
 
+format pretty_fn::pp_binder(expr const & local) {
+    format r;
+    auto bi = local_info(local);
+    if (bi != binder_info())
+        r += format(open_binder_string(bi, m_unicode));
+    r += format(local_pp_name(local));
+    r += space();
+    r += compose(colon(), nest(m_indent, compose(line(), pp_child(mlocal_type(local), 0).fmt())));
+    if (bi != binder_info())
+        r += format(close_binder_string(bi, m_unicode));
+    return r;
+}
+
 format pretty_fn::pp_binder_block(buffer<name> const & names, expr const & type, binder_info const & bi) {
     format r;
     r += format(open_binder_string(bi, m_unicode));
@@ -1123,7 +1136,9 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
             case notation::action_kind::Binder:
                 if (locals.size() != 1)
                     return optional<result>();
-                curr = format(tk) + pp_binders(locals);
+                curr = format(tk) + pp_binder(locals[0]);
+                if (!last)
+                    curr = curr + space();
                 break;
             case notation::action_kind::Binders:
                 curr = format(tk) + pp_binders(locals);

src/frontends/lean/pp.h

@@ -81,6 +81,7 @@ private:
     optional<name> is_aliased(name const & n) const;
     optional<name> is_abbreviated(expr const & e) const;
 
+    format pp_binder(expr const & local);
     format pp_binder_block(buffer<name> const & names, expr const & type, binder_info const & bi);
     format pp_binders(buffer<expr> const & locals);
     format pp_level(level const & l);

tests/lean/630.lean.expected.out

@@ -1,5 +1,5 @@
 definition pnat.pnat : Type₁ :=
-{ (n : ℕ)| nat.gt n (nat.of_num 0)}
+{n : ℕ | nat.gt n (nat.of_num 0)}
 inductive prod : Type → Type → Type
 constructors:
 prod.mk : Π {A : Type} {B : Type}, A → B → A × B

tests/lean/print_ax2.lean.expected.out

@@ -1,3 +1,3 @@
 quot.sound : ∀ {A : Type} [s : setoid A] {a b : A}, setoid.r a b → quot.mk a = quot.mk b
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
-strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A)| Exists P → P x}
+strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → {x : A | Exists P → P x}

tests/lean/subpp.lean

@@ -0,0 +1,4 @@
+import data.subtype
+open nat
+
+check {x : nat| x > 0 }

tests/lean/subpp.lean.expected.out

@@ -0,0 +1 @@
+{x : ℕ | x > 0} : Type₁