feat: delaborator: use ∀ if prop

src/Lean/Parser/Term.lean

@@ -97,7 +97,8 @@ def binderDefault := parser! " := " >> termParser
 def explicitBinder (requireType := false) := ppGroup $ parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
 def implicitBinder (requireType := false) := ppGroup $ parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
 def instBinder := ppGroup $ parser! "[" >> optIdent >> termParser >> "]"
-def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder
+def bracketedBinder (requireType := false) := withAntiquot (mkAntiquot "bracketedBinder" none (anonymous := false)) <|
+  explicitBinder requireType <|> implicitBinder requireType <|> instBinder
 
 /-
 It is feasible to support dependent arrows such as `{α} → α → α` without sacrificing the quality of the error messages for the longer case.
@@ -118,7 +119,7 @@ Note that we did not add a `explicitShortBinder` parser since `(α) → α →
 
 def simpleBinder := parser! many1 binderIdent >> optType
 @[builtinTermParser]
-def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser
+def «forall» := parser!:leadPrec unicodeSymbol "∀" "forall" >> many1 (ppSpace >> (simpleBinder <|> bracketedBinder)) >> ", " >> termParser
 
 def matchAlt (rhsParser : Parser := termParser) : Parser :=
   nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -108,7 +108,7 @@ def delabAppExplicit : Delab := do
       let fn ← getExpr
       let stx ← if fn.isConst then delabConst else delab
       let paramKinds ← liftM <| getParamKinds fn <|> pure #[]
-      let stx ← if paramKinds.any (fun k => match k with | ParamKind.explicit => false | _ => true) = true then `(@$stx) else pure stx
+      let stx ← if paramKinds.any (fun | ParamKind.explicit => false | _ => true) = true then `(@$stx) else pure stx
       pure (stx, #[]))
     (fun ⟨fnStx, argStxs⟩ => do
       let argStx ← delab
@@ -350,21 +350,31 @@ def delabLam : Delab :=
 def delabForall : Delab :=
   delabBinders fun curNames stxBody => do
     let e ← getExpr
+    let prop ← try isProp e catch _ => false
     let stxT ← withBindingDomain delab
-    match e.binderInfo with
+    let group ← match e.binderInfo with
     | BinderInfo.default      =>
       -- heuristic: use non-dependent arrows only if possible for whole group to avoid
       -- noisy mix like `(α : Type) → Type → (γ : Type) → ...`.
       let dependent := curNames.any $ fun n => hasIdent n.getId stxBody
       -- NOTE: non-dependent arrows are available only for the default binder info
-      if dependent then do
-        `(($curNames* : $stxT) → $stxBody)
+      if dependent then
+        if prop && !(← getPPOption getPPBinderTypes) then
+          return ← `(∀ $curNames:ident*, $stxBody)
+        else
+          `(bracketedBinderF|($curNames* : $stxT))
       else
-        curNames.foldrM (fun _ stxBody => `($stxT → $stxBody)) stxBody
-    | BinderInfo.implicit     => `({$curNames* : $stxT} → $stxBody)
+        return ← curNames.foldrM (fun _ stxBody => `($stxT → $stxBody)) stxBody
+    | BinderInfo.implicit     => `(bracketedBinderF|{$curNames* : $stxT})
     -- here `curNames.size == 1`
-    | BinderInfo.instImplicit => `([$curNames.back : $stxT] → $stxBody)
+    | BinderInfo.instImplicit => `(bracketedBinderF|[$curNames.back : $stxT])
     | _                       => unreachable!
+    if prop then
+      match stxBody with
+      | `(∀ $groups*, $stxBody) => `(∀ $group $groups*, $stxBody)
+      | _                       => `(∀ $group, $stxBody)
+    else
+      `($group:bracketedBinder → $stxBody)
 
 @[builtinDelab letE]
 def delabLetE : Delab := do

tests/lean/223.lean.expected.out

@@ -2,7 +2,7 @@ def h.{u_1, u_2} : {α : Type u_1} → {β : Type u_2} → {f : α → β} → {
 fun {α : Type u_1} {β : Type u_2} {f : α → β} (x : β) (x_1 : Imf f x) =>
   match x, x_1 with 
   | .(f a), Imf.mk a => a
-theorem ex.{u} : {α β : Sort u} → (h : α = β) → (a : α) → cast h a ≅ a :=
+theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a :=
 fun (x x_1 : Sort u) (x_2 : x = x_1) (x_3 : x) =>
   match x, x_1, x_2, x_3 with 
   | α, .(α), Eq.refl α, a => HEq.refl a

tests/lean/PPRoundtrip.lean

@@ -73,9 +73,12 @@ end
 #eval checkM `((α β : Type) → α)  -- group
 #eval checkM `((α β : Type) → Type)  -- don't group
 #eval checkM `((α : Type) → (a : α) → α)
-#eval checkM `((α : Type) → (a : α) → a = a)
 #eval checkM `({α : Type} → α)
 #eval checkM `({α : Type} → [ToString α] → α)
+#eval checkM `(∀ x : Nat, x = x)
+#eval checkM `(∀ {x : Nat} [ToString Nat], x = x)
+set_option pp.binder_types false in
+#eval checkM `(∀ x : Nat, x = x)
 
 -- TODO: hide `ofNat`
 #eval checkM `(0)

tests/lean/PPRoundtrip.lean.expected.out

@@ -31,13 +31,17 @@ fun {α : Type}
 (α β : Type) → α
 Type → Type → Type
 (α : Type) → α → α
-(α : Type) →
-  (a : α) → a = a
 {α : Type} → α
 {α : Type} →
   [inst :
       ToString α] →
     α
+∀ (x : Nat), x = x
+∀ {x : Nat}
+  [inst :
+    ToString Nat],
+  x = x
+∀ x, x = x
 0
 1
 42

tests/lean/Reformat.lean.expected.out

@@ -230,7 +230,7 @@ structure PLift(α : Sort u) : Type u := up ::
   (down : α)
 
 /- Bijection between α and PLift α -/
-theorem PLift.upDown {α : Sort u} : ∀  (b : PLift α), Eq (up (down b)) b
+theorem PLift.upDown {α : Sort u} : ∀ (b : PLift α), Eq (up (down b)) b
 | up a => rfl 
 
 theorem PLift.downUp {α : Sort u} (a : α) : Eq (down (up a)) a :=
@@ -249,7 +249,7 @@ structure ULift.{r, s}(α : Type s) : Type (max s r) := up ::
   (down : α)
 
 /- Bijection between α and ULift.{v} α -/
-theorem ULift.upDown {α : Type u} : ∀  (b : ULift.{v} α), Eq (up (down b)) b
+theorem ULift.upDown {α : Type u} : ∀ (b : ULift.{v} α), Eq (up (down b)) b
 | up a => rfl 
 
 theorem ULift.downUp {α : Type u} (a : α) : Eq (down (up.{v} a)) a :=

tests/lean/precissues.lean.expected.out

@@ -21,6 +21,6 @@ p ∧ ¬q : Prop
 ¬p = q : Prop
 ¬p = q : Prop
 id ¬p : Prop
-(a a : Nat) → a = a : Prop
+∀ (a a : Nat), a = a : Prop
 id : ?m → ?m
 precissues.lean:41:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term

tests/lean/sizeof.lean.expected.out

@@ -7,5 +7,5 @@
 308
 310
 11
-InfTree.node.sizeOf_spec : {α : Type u_1} →
-  [inst : SizeOf α] → (children : Nat → InfTree α) → sizeOf (InfTree.node children) = 1
+InfTree.node.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (children : Nat → InfTree α),
+  sizeOf (InfTree.node children) = 1