cleanup diff

src/Lean/Elab/Tactic/Simp.lean

@@ -155,9 +155,9 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind :
           else
             let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
             if ctx.config.autoUnfold then
-              thms := thms.eraseCore (.decl declName false)
+              thms := thms.eraseCore (.decl declName)
             else
-              thms ← thms.erase (.decl declName false)
+              thms ← thms.erase (.decl declName)
         else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
           let post :=
             if arg[0].isNone then

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -100,7 +100,7 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
           -/
           let e? ← withReducibleAndInstances <| unfoldDefinition? e
           if e?.isSome then
-            recordSimpTheorem (.decl cinfo.name false)
+            recordSimpTheorem (.decl cinfo.name)
           return e?
         else
           /-
@@ -154,7 +154,7 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
     return none -- should be reduced by `reduceProjFn?`
   let ctx ← read
   if ctx.config.autoUnfold then
-    if ctx.simpTheorems.isErased (.decl fName false) then
+    if ctx.simpTheorems.isErased (.decl fName) then
       return none
     else if hasSmartUnfoldingDecl (← getEnv) fName then
       withDefault <| unfoldDefinition? e
@@ -191,7 +191,7 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
   match (← unfold? e) with
   | some e' =>
     trace[Meta.Tactic.simp.rewrite] "unfold {mkConst e.getAppFn.constName!}, {e} ==> {e'}"
-    recordSimpTheorem (.decl e.getAppFn.constName! false)
+    recordSimpTheorem (.decl e.getAppFn.constName!)
     reduce e'
   | none => return e
 
@@ -571,7 +571,7 @@ where
       unless modified do
         trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified"
         return none
-      unless (← synthesizeArgs (.decl c.theoremName false) xs bis (← read).discharge?) do
+      unless (← synthesizeArgs (.decl c.theoremName) xs bis (← read).discharge?) do
         trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed"
         return none
       let eNew ← instantiateMVars rhs

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -224,7 +224,7 @@ def simpArith? (e : Expr) : SimpM (Option Step) := do
 def simpMatchCore? (app : MatcherApp) (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Step) := do
   for matchEq in (← Match.getEquationsFor app.matcherName).eqnNames do
     -- Try lemma
-    match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq false, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) } discharge?) with
+    match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) } discharge?) with
     | none   => pure ()
     | some r => return some (Simp.Step.done r)
   return none

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -186,10 +186,10 @@ def SimpTheorems.registerDeclToUnfoldThms (d : SimpTheorems) (declName : Name) (
 
 partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpTheorems :=
   let d := { d with erased := d.erased.insert thmId, lemmaNames := d.lemmaNames.erase thmId }
-  if let .decl declName false := thmId then
+  if let .decl declName := thmId then
     let d := { d with toUnfold := d.toUnfold.erase declName }
     if let some thms := d.toUnfoldThms.find? declName then
-      thms.foldl (init := d) (eraseCore · <| .decl · false)
+      thms.foldl (init := d) (eraseCore · <| .decl ·)
     else
       d
   else
@@ -198,7 +198,7 @@ partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpThe
 def SimpTheorems.erase [Monad m] [MonadError m] (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do
   unless d.isLemma thmId ||
     match thmId with
-    | .decl declName false => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName
+    | .decl declName => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName
     | _ => false
   do
     throwError "'{thmId.key}' does not have [simp] attribute"
@@ -321,7 +321,7 @@ private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool)
         r := r.push <| (← mkSimpTheoremCore (.decl declName inv) (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio)
       return r
     else
-      return #[← mkSimpTheoremCore (.decl declName false) (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio]
+      return #[← mkSimpTheoremCore (.decl declName) (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio]
 
 inductive SimpEntry where
   | thm      : SimpTheorem → SimpEntry
@@ -367,7 +367,7 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
       discard <| go.run {} {}
     erase := fun declName => do
       let s := ext.getState (← getEnv)
-      let s ← s.erase (.decl declName false)
+      let s ← s.erase (.decl declName)
       modifyEnv fun env => ext.modifyState env fun _ => s
   }
 

src/Lean/Meta/Tactic/Split.lean

@@ -47,7 +47,7 @@ where
       | none    =>
       -- Try lemma
       let simpTheorem := {
-        origin := .decl matchEqDeclName false
+        origin := .decl matchEqDeclName
         proof := mkConst matchEqDeclName
         rfl := (← isRflTheorem matchEqDeclName)
       }

src/Lean/Meta/Tactic/Unfold.lean

@@ -22,7 +22,7 @@ def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
     return { expr  := (← deltaExpand e (· == declName)) }
 where
   pre (unfoldThm : Name) (e : Expr) : SimpM Simp.Step := do
-    match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm false, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm) } (fun _ => return none)) with
+    match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm) } (fun _ => return none)) with
     | none   => pure ()
     | some r => match (← reduceMatcher? r.expr) with
       | .reduced e' => return Simp.Step.done { r with expr := e' }

tests/lean/run/simp1.lean

@@ -46,7 +46,7 @@ def tst2 : MetaM Unit := do
       let s ← Meta.getSimpTheorems
       let m ← s.post.getMatch lhs
       trace[Meta.debug] "result: {m}"
-      assert! m.any fun s => s.origin == .decl `ex2 false
+      assert! m.any fun s => s.origin == .decl `ex2
 
 
 set_option trace.Meta.debug true in