feat(frontends/lean/pp): pretty print set_of notation

src/frontends/lean/pp.cpp

@@ -1510,6 +1510,26 @@ auto pretty_fn::pp_explicit_collection(buffer<expr> const & elems) -> result {
     return result(r);
 }
 
+bool is_set_of(expr const & e) {
+    return
+        is_constant(get_app_fn(e), get_set_of_name()) &&
+        get_app_num_args(e) == 2 &&
+        is_lambda(app_arg(e));
+}
+
+auto pretty_fn::pp_set_of(expr const & e) -> result {
+    lean_assert(is_set_of(e));
+    expr pred = app_arg(e);
+    lean_assert(is_lambda(pred));
+    auto p     = binding_body_fresh(pred, true);
+    expr body  = p.first;
+    expr local = p.second;
+    format r   = bracket("{",
+                         pp_binder(local) + space() + format("|") + space() +
+                         pp_child(body, 0).fmt(), "}");
+    return result(r);
+}
+
 static bool is_sep(expr const & e) {
     return
         is_constant(get_app_fn(e), get_sep_name()) &&
@@ -1563,6 +1583,8 @@ auto pretty_fn::pp(expr const & e, bool ignore_hide) -> result {
             return pp_subtype(e);
         if (is_sep(e))
             return pp_sep(e);
+        if (is_set_of(e))
+            return pp_set_of(e);
         buffer<expr> elems;
         if (is_explicit_collection(e, elems))
             return pp_explicit_collection(elems);

src/frontends/lean/pp.h

@@ -116,6 +116,7 @@ private:
     result pp_child(expr const & e, unsigned bp, bool ignore_hide = false);
     result pp_subtype(expr const & e);
     result pp_sep(expr const & e);
+    result pp_set_of(expr const & e);
     result pp_explicit_collection(buffer<expr> const & elems);
     result pp_var(expr const & e);
     result pp_sort(expr const & e);

tests/lean/set_of.lean

@@ -0,0 +1,9 @@
+check {x : nat | x > 0}
+check {x | x > 0}
+check {p : nat × nat | p.1 > p.2 }
+
+set_option pp.binder_types false
+
+check {x : nat | x > 0}
+check {x | x > 0}
+check {p : nat × nat | p.1 > p.2 }

tests/lean/set_of.lean.expected.out

@@ -0,0 +1,6 @@
+{x : ℕ | x > 0} : set ℕ
+{x : ℕ | x > 0} : set ℕ
+{p : ℕ × ℕ | prod.fst p > prod.snd p} : set (ℕ × ℕ)
+{x | x > 0} : set ℕ
+{x | x > 0} : set ℕ
+{p | prod.fst p > prod.snd p} : set (ℕ × ℕ)