From fa9b0f6c7e6ec0c3b1d6e14ec989e2fc01efa4a3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 7 Apr 2022 07:54:17 -0700
Subject: [PATCH] feat: remove space before propositions with inaccessible
 names

---
 src/Lean/Meta/PPGoal.lean                     | 28 +++++++++----------
 src/Lean/Widget/InteractiveGoal.lean          | 16 +++++++----
 tests/lean/1074b.lean.expected.out            |  2 +-
 tests/lean/361.lean.expected.out              |  4 +--
 tests/lean/badIhName.lean.expected.out        |  2 +-
 tests/lean/bintreeGoal.lean.expected.out      | 10 +++----
 .../hidingInaccessibleNames.lean.expected.out | 16 +++++------
 tests/lean/inductionGen.lean.expected.out     |  8 +++---
 tests/lean/interactive/anonHyp.lean           |  4 +++
 .../interactive/anonHyp.lean.expected.out     |  5 ++++
 .../interactive/plainGoal.lean.expected.out   |  4 +--
 tests/lean/lean3RefineBug.lean.expected.out   |  4 +--
 tests/lean/rewrite.lean.expected.out          |  2 +-
 .../tacUnsolvedGoalsErrors.lean.expected.out  |  8 +++---
 tests/lean/unknownTactic.lean.expected.out    |  2 +-
 tests/lean/wf2.lean.expected.out              |  2 +-
 16 files changed, 65 insertions(+), 52 deletions(-)
 create mode 100644 tests/lean/interactive/anonHyp.lean
 create mode 100644 tests/lean/interactive/anonHyp.lean.expected.out

diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index 16ce1e8d7f..3c9e6e3b50 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -164,8 +164,8 @@ private def addLine (fmt : Format) : Format :=
 
 def ppGoal (mvarId : MVarId) : MetaM Format := do
   match (← getMCtx).findDecl? mvarId with
-  | none          => pure "unknown goal"
-  | some mvarDecl => do
+  | none          => return "unknown goal"
+  | some mvarDecl =>
     let indent         := 2 -- Use option
     let ppAuxDecls     := pp.auxDecls.get (← getOptions)
     let lctx           := mvarDecl.lctx
@@ -174,34 +174,34 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
       let (hidden, hiddenProp) ← ToHide.collect mvarDecl.type
       -- The followint two `let rec`s are being used to control the generated code size.
       -- Then should be remove after we rewrite the compiler in Lean
-      let rec pushPending (ids : List Name) (type? : Option Expr) (fmt : Format) : MetaM Format :=
+      let rec pushPending (ids : List Name) (type? : Option Expr) (fmt : Format) : MetaM Format := do
         if ids.isEmpty then
-          pure fmt
+          return fmt
         else
           let fmt := addLine fmt
           match type? with
-          | none      => pure fmt
-          | some type => do
+          | none      => return fmt
+          | some type =>
             let typeFmt ← ppExpr type
-            pure $ fmt ++ (Format.joinSep ids.reverse (format " ") ++ " :" ++ Format.nest indent (Format.line ++ typeFmt)).group
+            return fmt ++ (Format.joinSep ids.reverse (format " ") ++ " :" ++ Format.nest indent (Format.line ++ typeFmt)).group
       let rec ppVars (varNames : List Name) (prevType? : Option Expr) (fmt : Format) (localDecl : LocalDecl) : MetaM (List Name × Option Expr × Format) := do
         if hiddenProp.contains localDecl.fvarId then
           let fmt ← pushPending varNames prevType? fmt
           let fmt  := addLine fmt
           let type ← instantiateMVars localDecl.type
           let typeFmt ← ppExpr type
-          let fmt  := fmt ++ " : " ++ typeFmt
-          pure ([], none, fmt)
+          let fmt  := fmt ++ ": " ++ typeFmt
+          return ([], none, fmt)
         else
           match localDecl with
           | LocalDecl.cdecl _ _ varName type _   =>
             let varName := varName.simpMacroScopes
             let type ← instantiateMVars type
             if prevType? == none || prevType? == some type then
-              pure (varName :: varNames, some type, fmt)
+              return (varName :: varNames, some type, fmt)
             else do
               let fmt ← pushPending varNames prevType? fmt
-              pure ([varName], some type, fmt)
+              return ([varName], some type, fmt)
           | LocalDecl.ldecl _ _ varName type val _ => do
             let varName := varName.simpMacroScopes
             let fmt ← pushPending varNames prevType? fmt
@@ -211,10 +211,10 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
             let typeFmt ← ppExpr type
             let valFmt ← ppExpr val
             let fmt  := fmt ++ (format varName ++ " : " ++ typeFmt ++ " :=" ++ Format.nest indent (Format.line ++ valFmt)).group
-            pure ([], none, fmt)
+            return ([], none, fmt)
       let (varNames, type?, fmt) ← lctx.foldlM (init := ([], none, Format.nil)) fun (varNames, prevType?, fmt) (localDecl : LocalDecl) =>
          if !ppAuxDecls && localDecl.isAuxDecl || hidden.contains localDecl.fvarId then
-           pure (varNames, prevType?, fmt)
+           return (varNames, prevType?, fmt)
          else
            ppVars varNames prevType? fmt localDecl
       let fmt ← pushPending varNames type? fmt
@@ -222,7 +222,7 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
       let typeFmt ← ppExpr (← instantiateMVars mvarDecl.type)
       let fmt := fmt ++ "⊢ " ++ Format.nest indent typeFmt
       match mvarDecl.userName with
-      | Name.anonymous => pure fmt
+      | Name.anonymous => return fmt
       | name           => return "case " ++ format name.eraseMacroScopes ++ Format.line ++ fmt
 
 end Lean.Meta
diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index 4709ab31e3..053288ec22 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -38,12 +38,16 @@ def pretty (g : InteractiveGoal) : Format := Id.run <| do
     | none          => Format.nil
   for hyp in g.hyps do
     ret := addLine ret
-    let names := " ".intercalate hyp.names.toList
-    match hyp.val? with
-    | some val =>
-      ret := ret ++ Format.group f!"{names} : {hyp.type.stripTags} :={Format.nest indent (Format.line ++ val.stripTags)}"
-    | none =>
-      ret := ret ++ Format.group f!"{names} :{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
+    match hyp.names.toList with
+    | [] =>
+      ret := ret ++ Format.group f!":{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
+    | _ =>
+      let names := " ".intercalate hyp.names.toList
+      match hyp.val? with
+      | some val =>
+        ret := ret ++ Format.group f!"{names} : {hyp.type.stripTags} :={Format.nest indent (Format.line ++ val.stripTags)}"
+      | none =>
+        ret := ret ++ Format.group f!"{names} :{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
   ret := addLine ret
   ret ++ f!"⊢ {Format.nest indent g.type.stripTags}"
 
diff --git a/tests/lean/1074b.lean.expected.out b/tests/lean/1074b.lean.expected.out
index 3c26cf4a4f..2b7e9055a6 100644
--- a/tests/lean/1074b.lean.expected.out
+++ b/tests/lean/1074b.lean.expected.out
@@ -5,5 +5,5 @@ a n : Term
 1074b.lean:11:9-11:55: error: unsolved goals
 case id
 a n z✝ : Term
- : Brx z✝
+: Brx z✝
 ⊢ True ∧ Brx (sorryAx Term)
diff --git a/tests/lean/361.lean.expected.out b/tests/lean/361.lean.expected.out
index 42bc29bdac..f29bf71c46 100644
--- a/tests/lean/361.lean.expected.out
+++ b/tests/lean/361.lean.expected.out
@@ -8,11 +8,11 @@ h2 : p → q
 361.lean:5:11-5:13: error: unsolved goals
 p q r : Prop
 h2 : p → q
- : p
+: p
 ⊢ q
 361.lean:3:60-5:13: error: unsolved goals
 case inr
 p q r : Prop
 h2 : p → q
- : q
+: q
 ⊢ q
diff --git a/tests/lean/badIhName.lean.expected.out b/tests/lean/badIhName.lean.expected.out
index 909aeca8d1..930dfc3062 100644
--- a/tests/lean/badIhName.lean.expected.out
+++ b/tests/lean/badIhName.lean.expected.out
@@ -4,5 +4,5 @@ case z
 
 case s
 a✝ : Nat
- : add Nat.z a✝ = a✝
+: add Nat.z a✝ = a✝
 ⊢ add Nat.z (Nat.s a✝) = Nat.s a✝
diff --git a/tests/lean/bintreeGoal.lean.expected.out b/tests/lean/bintreeGoal.lean.expected.out
index 51a5623109..7dd19555b7 100644
--- a/tests/lean/bintreeGoal.lean.expected.out
+++ b/tests/lean/bintreeGoal.lean.expected.out
@@ -11,10 +11,10 @@ value : β
 right : Tree β
 ihl : BST left → Tree.find? (Tree.insert left k v) k = some v
 ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
- : k < key
- : BST left
- : ForallTree (fun k v => k < key) left
- : BST right
- : ForallTree (fun k v => key < k) right
+: k < key
+: BST left
+: ForallTree (fun k v => k < key) left
+: BST right
+: ForallTree (fun k v => key < k) right
 ⊢ BST left
 bintreeGoal.lean:67:6-67:11: warning: declaration uses 'sorry'
diff --git a/tests/lean/hidingInaccessibleNames.lean.expected.out b/tests/lean/hidingInaccessibleNames.lean.expected.out
index fedfda2532..64511de41b 100644
--- a/tests/lean/hidingInaccessibleNames.lean.expected.out
+++ b/tests/lean/hidingInaccessibleNames.lean.expected.out
@@ -4,42 +4,42 @@ context:
 hidingInaccessibleNames.lean:3:19-3:20: error: don't know how to synthesize placeholder
 context:
 a b : Nat
- : [a, b] ≠ []
+: [a, b] ≠ []
 ⊢ Nat
 hidingInaccessibleNames.lean:2:16-2:17: error: don't know how to synthesize placeholder
 context:
- : [] ≠ []
+: [] ≠ []
 ⊢ Nat
 hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
 context:
 a b x✝¹ : Nat
- : [a, b] ≠ []
+: [a, b] ≠ []
 ⊢ Nat
 hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder
 context:
 x✝¹ : Nat
- : [] ≠ []
+: [] ≠ []
 ⊢ Nat
 hidingInaccessibleNames.lean:10:16-10:17: error: don't know how to synthesize placeholder
 context:
 x✝² : List Nat
 x✝¹ : Nat
- : x✝² ≠ []
+: x✝² ≠ []
 ⊢ Nat
 case inl
 p q : Prop
- : p
+: p
 ⊢ q ∨ p
 
 case inr
 p q : Prop
- : q
+: q
 ⊢ q ∨ p
 hidingInaccessibleNames.lean:23:25-23:26: error: don't know how to synthesize placeholder
 context:
 x✝² : Prop
 x✝¹ : x✝²
- : x✝²
+: x✝²
 ⊢ decide x✝² = true
 hidingInaccessibleNames.lean:27:17-27:18: error: don't know how to synthesize placeholder
 context:
diff --git a/tests/lean/inductionGen.lean.expected.out b/tests/lean/inductionGen.lean.expected.out
index 8a48f4d290..b71fd325ea 100644
--- a/tests/lean/inductionGen.lean.expected.out
+++ b/tests/lean/inductionGen.lean.expected.out
@@ -30,8 +30,8 @@ h : Expr.boolVal a✝ = b
 case eq
 α α✝ : ExprType
 a✝¹ a✝ : Expr α✝
- : ∀ (b : Expr α✝), a✝¹ = b → eval (constProp a✝¹) = eval b
- : ∀ (b : Expr α✝), a✝ = b → eval (constProp a✝) = eval b
+: ∀ (b : Expr α✝), a✝¹ = b → eval (constProp a✝¹) = eval b
+: ∀ (b : Expr α✝), a✝ = b → eval (constProp a✝) = eval b
 b : Expr ExprType.bool
 h : Expr.eq a✝¹ a✝ = b
 ⊢ eval (constProp (Expr.eq a✝¹ a✝)) = eval b
@@ -39,8 +39,8 @@ h : Expr.eq a✝¹ a✝ = b
 case add
 α : ExprType
 a✝¹ a✝ : Expr ExprType.nat
- : ∀ (b : Expr ExprType.nat), a✝¹ = b → eval (constProp a✝¹) = eval b
- : ∀ (b : Expr ExprType.nat), a✝ = b → eval (constProp a✝) = eval b
+: ∀ (b : Expr ExprType.nat), a✝¹ = b → eval (constProp a✝¹) = eval b
+: ∀ (b : Expr ExprType.nat), a✝ = b → eval (constProp a✝) = eval b
 b : Expr ExprType.nat
 h : Expr.add a✝¹ a✝ = b
 ⊢ eval (constProp (Expr.add a✝¹ a✝)) = eval b
diff --git a/tests/lean/interactive/anonHyp.lean b/tests/lean/interactive/anonHyp.lean
new file mode 100644
index 0000000000..6c78325a6f
--- /dev/null
+++ b/tests/lean/interactive/anonHyp.lean
@@ -0,0 +1,4 @@
+example (x : Nat) : x + 1 > 0 := by
+  induction x
+  decide
+  --^ $/lean/plainGoal
diff --git a/tests/lean/interactive/anonHyp.lean.expected.out b/tests/lean/interactive/anonHyp.lean.expected.out
new file mode 100644
index 0000000000..765476adca
--- /dev/null
+++ b/tests/lean/interactive/anonHyp.lean.expected.out
@@ -0,0 +1,5 @@
+{"textDocument": {"uri": "file://anonHyp.lean"},
+ "position": {"line": 2, "character": 4}}
+{"rendered":
+ "```lean\ncase succ\nn✝ : Nat\n: n✝ + 1 > 0\n⊢ Nat.succ n✝ + 1 > 0\n```",
+ "goals": ["case succ\nn✝ : Nat\n: n✝ + 1 > 0\n⊢ Nat.succ n✝ + 1 > 0"]}
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index 06917dd84c..9fa4746e58 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -29,9 +29,9 @@
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 17, "character": 5}}
 {"rendered":
- "```lean\ncase succ\nn✝ : Nat\n : 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝\n```",
+ "```lean\ncase succ\nn✝ : Nat\n: 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝\n```",
  "goals":
- ["case succ\nn✝ : Nat\n : 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝"]}
+ ["case succ\nn✝ : Nat\n: 0 + n✝ = n✝\n⊢ 0 + Nat.succ n✝ = Nat.succ n✝"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 21, "character": 9}}
 {"rendered": "```lean\nα : Sort ?u\na : α\n⊢ α\n```",
diff --git a/tests/lean/lean3RefineBug.lean.expected.out b/tests/lean/lean3RefineBug.lean.expected.out
index f5d310438d..de10516c99 100644
--- a/tests/lean/lean3RefineBug.lean.expected.out
+++ b/tests/lean/lean3RefineBug.lean.expected.out
@@ -4,13 +4,13 @@ a : p ∧ q
 ⊢ p
 case hp
 p q : Prop
- : p ∧ q
+: p ∧ q
 a : p
 b : q
 ⊢ p
 case hp
 p q : Prop
- : p ∧ q
+: p ∧ q
 a : p
 b : q
 ⊢ p
diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out
index c619e3c911..3bc17b2d53 100644
--- a/tests/lean/rewrite.lean.expected.out
+++ b/tests/lean/rewrite.lean.expected.out
@@ -16,7 +16,7 @@ h₁ : 0 + x = y
 h₂ : 0 + y = z
 ⊢ x = z
 m n k : Nat
- : n = m
+: n = m
 h : k = m
 ⊢ k = n
 rewrite.lean:49:69-50:10: error: unsolved goals
diff --git a/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out b/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out
index cff2365619..6b52456edb 100644
--- a/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out
+++ b/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out
@@ -24,23 +24,23 @@ tacUnsolvedGoalsErrors.lean:17:9-17:10: error: unsolved goals
 case inl
 p q r : Prop
 h2 : p → q
- : p
+: p
 ⊢ q
 tacUnsolvedGoalsErrors.lean:19:9-19:10: error: unsolved goals
 case inr
 p q r : Prop
 h2 : p → q
- : q
+: q
 ⊢ q
 tacUnsolvedGoalsErrors.lean:26:2-27:8: error: unsolved goals
 case inl
 p q r : Prop
 h2 : p → q
- : p
+: p
 ⊢ q
 tacUnsolvedGoalsErrors.lean:28:2-29:8: error: unsolved goals
 case inr
 p q r : Prop
 h2 : p → q
- : q
+: q
 ⊢ q
diff --git a/tests/lean/unknownTactic.lean.expected.out b/tests/lean/unknownTactic.lean.expected.out
index 298595ead6..ea988bf2f1 100644
--- a/tests/lean/unknownTactic.lean.expected.out
+++ b/tests/lean/unknownTactic.lean.expected.out
@@ -1,7 +1,7 @@
 unknownTactic.lean:3:3: error: unknown tactic
 unknownTactic.lean:1:41-3:8: error: unsolved goals
 x : Nat
- : x = x
+: x = x
 ⊢ x = x
 ---
 unknownTactic.lean:8:22: error: unknown tactic
diff --git a/tests/lean/wf2.lean.expected.out b/tests/lean/wf2.lean.expected.out
index fe427e05f2..bdf452385e 100644
--- a/tests/lean/wf2.lean.expected.out
+++ b/tests/lean/wf2.lean.expected.out
@@ -3,5 +3,5 @@ wf2.lean:3:8-3:17: error: failed to prove termination, possible solutions:
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
 x y : Nat
- : x < y
+: x < y
 ⊢ x - 1 < x