chore: add explicit discard

src/Init/Control/Basic.lean

@@ -13,7 +13,7 @@ universes u v w
 
 infixr:100 " <&> " => Functor.mapRev
 
-def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit :=
+@[inline] def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit :=
   Functor.mapConst PUnit.unit x
 
 export Functor (discard)

src/Lean/Compiler/IR/EmitC.lean

@@ -383,7 +383,7 @@ def toStringArgs (ys : Array Arg) : List String :=
 def emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M Unit := do
   emit f; emit "("
   -- We must remove irrelevant arguments to extern calls.
-  ys.size.foldM
+  discard <| ys.size.foldM
     (fun i (first : Bool) =>
       if ps[i].ty.isIrrelevant then
         pure first

src/Lean/Elab/App.lean

@@ -336,8 +336,7 @@ private def finalize : M Expr := do
   | some expectedType =>
      trace[Elab.app.finalize]! "expected type: {expectedType}"
      -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it.
-     isDefEq expectedType eType
-     pure ()
+     discard <| isDefEq expectedType eType
   synthesizeAppInstMVars
   pure e
 

src/Lean/Elab/Binders.lean

@@ -298,7 +298,7 @@ private def propagateExpectedType (fvar : Expr) (fvarType : Expr) (s : State) :
     let expectedType ← whnfForall expectedType
     match expectedType with
     | Expr.forallE _ d b _ =>
-      isDefEq fvarType d
+      discard <| isDefEq fvarType d
       let b := b.instantiate1 fvar
       pure { s with expectedType? := some b }
     | _ => pure { s with expectedType? := none }

src/Lean/Elab/BuiltinNotation.lean

@@ -322,7 +322,7 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
   let m ← elabTerm m (← mkArrow (mkSort levelOne) (mkSort levelOne))
   let ω ← mkFreshExprMVar (mkSort levelOne)
   let stWorld ← mkAppM `STWorld #[ω, m]
-  mkInstMVar stWorld
+  discard <| mkInstMVar stWorld
   mkAppM `StateRefT' #[ω, σ, m]
 
 end Lean.Elab.Term

src/Lean/Elab/Match.lean

@@ -471,7 +471,7 @@ partial def collect : Syntax → M Syntax
       /- Recall that
          def namedPattern := check... >> tparser! "@" >> termParser -/
       let id := stx[0]
-      processVar id
+      discard <| processVar id
       let pat := stx[2]
       let pat ← collect pat
       `(namedPattern $id $pat)
@@ -521,8 +521,7 @@ def getPatternVars (patternStx : Syntax) : TermElabM (Array PatternVar) := do
 def getPatternsVars (patterns : Array Syntax) : TermElabM (Array PatternVar) := do
   let collect : CollectPatternVars.M Unit := do
     for pattern in patterns do
-      CollectPatternVars.collect (← liftMacroM $ expandMacros pattern)
-      pure ()
+      discard <| CollectPatternVars.collect (← liftMacroM $ expandMacros pattern)
   let (_, s) ← collect.run {}
   pure s.vars
 
@@ -552,8 +551,7 @@ private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array P
       decls.forM fun decl => match decl with
         | PatternVarDecl.anonymousVar mvarId fvarId => do
           let type ← inferType (mkFVar fvarId)
-          mkFreshExprMVarWithId mvarId type
-          pure ()
+          discard <| mkFreshExprMVarWithId mvarId type
         | _ => pure ()
       k decls
   loop 0 #[]

src/Lean/Elab/StructInst.lean

@@ -504,8 +504,7 @@ private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType?
       | none           => pure ()
       | some typeBody =>
         unless typeBody.hasLooseBVars do
-          isDefEq expectedType typeBody
-          pure ()
+          discard <| isDefEq expectedType typeBody
 
 private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do
   let lvls ← ctorVal.lparams.mapM fun _ => mkFreshLevelMVar

src/Lean/Elab/Structure.lean

@@ -339,8 +339,7 @@ private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldI
 
 private def levelMVarToParamFVar (fvar : Expr) : StateRefT Nat TermElabM Unit := do
   let type ← inferType fvar
-  Term.levelMVarToParam' type
-  pure ()
+  discard <| Term.levelMVarToParam' type
 
 private def levelMVarToParamFVars (fvars : Array Expr) : StateRefT Nat TermElabM Unit :=
   fvars.forM levelMVarToParamFVar
@@ -445,7 +444,7 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
     defaultAuxDecls.forM fun (declName, type, value) => do
       /- The identity function is used as "marker". -/
       let value ← mkId value
-      mkAuxDefinition declName type value (zeta := true)
+      discard <| mkAuxDefinition declName type value (zeta := true)
       setReducibleAttribute declName
 
 private def elabStructureView (view : StructView) : TermElabM Unit := do

src/Lean/Elab/Tactic/Basic.lean

@@ -184,7 +184,7 @@ def getMainTag : TacticM Name := do
 def ensureHasNoMVars (e : Expr) : TacticM Unit := do
   let e ← instantiateMVars e
   let pendingMVars ← getMVars e
-  Term.logUnassignedUsingErrorInfos pendingMVars
+  discard <| Term.logUnassignedUsingErrorInfos pendingMVars
   if e.hasExprMVar then
     throwError! "tactic failed, resulting expression contains metavariables{indentExpr e}"
 
@@ -244,8 +244,11 @@ def try? {α} (tactic : TacticM α) : TacticM (Option α) := do
 
 -- TODO: rename?
 def «try» {α} (tactic : TacticM α) : TacticM Bool := do
-  try tactic; pure true
-  catch _ => pure false
+  try
+    discard tactic
+    pure true
+  catch _ =>
+    pure false
 
 /--
   Use `parentTag` to tag untagged goals at `newGoals`.

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -48,7 +48,7 @@ def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix :
     else
       let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← getMVarDecl mvarId).kind.isNatural
       let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← getMVarDecl mvarId).kind.isNatural
-      Term.logUnassignedUsingErrorInfos naturalMVarIds
+      discard <| Term.logUnassignedUsingErrorInfos naturalMVarIds
       pure syntheticMVarIds.toList
   tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
   pure (val, newMVarIds)

src/Lean/Elab/Term.lean

@@ -1264,7 +1264,7 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL
 private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr := do
   let typeMVar ← mkFreshTypeMVar MetavarKind.synthetic
   match expectedType? with
-  | some expectedType => isDefEq expectedType typeMVar; pure ()
+  | some expectedType => discard <| isDefEq expectedType typeMVar
   | _                 => pure ()
   return typeMVar
 

src/Lean/Meta/Check.lean

@@ -14,8 +14,7 @@ whether terms produced by tactics and `isDefEq` are type correct.
 namespace Lean.Meta
 
 private def ensureType (e : Expr) : MetaM Unit := do
-  getLevel e
-  pure ()
+  discard <| getLevel e
 
 def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
   let lctx ← getLCtx

src/Lean/Meta/ExprDefEq.lean

@@ -166,9 +166,8 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
         let a₂   := args₂[i]
         let info := finfo.paramInfo[i]
         if info.instImplicit then
-          trySynthPending a₁
-          trySynthPending a₂
-          pure ()
+          discard <| trySynthPending a₁
+          discard <| trySynthPending a₂
         withAtLeastTransparency TransparencyMode.default $ Meta.isExprDefEqAux a₁ a₂
     else
       pure false

src/Lean/Meta/Instances.lean

@@ -56,8 +56,7 @@ builtin_initialize
     descr := "type class instance"
     add   := fun declName args attrKind => do
       if args.hasArgs then throwError "invalid attribute 'instance', unexpected argument"
-      addInstance declName attrKind |>.run {} {}
-      return ()
+      discard <| addInstance declName attrKind |>.run {} {}
   }
 
 @[export lean_is_instance]
@@ -123,8 +122,7 @@ builtin_initialize
         else
           throwErrorAt args "too many arguments at attribute 'defaultInstance', numeral expected"
       unless kind == AttributeKind.global do throwError "invalid attribute 'defaultInstance', must be global"
-      addDefaultInstance declName prio |>.run {} {}
-      pure ()
+      discard <| addDefaultInstance declName prio |>.run {} {}
   }
 
 def getDefaultInstancesPriorities [Monad m] [MonadEnv m] : m PrioritySet :=

src/Lean/Meta/Match/Match.lean

@@ -589,7 +589,7 @@ def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss :
     let matcher ← mkAuxDefinition matcherName type val (compile := generateMatcherCode (← getOptions))
     trace[Meta.Match.debug]! "matcher levels: {matcher.getAppFn.constLevels!}, uElim: {uElimGen}"
     let uElimPos? ← getUElimPos? matcher.getAppFn.constLevels! uElimGen
-    isLevelDefEq uElimGen uElim
+    discard <| isLevelDefEq uElimGen uElim
     addMatcherInfo matcherName { numParams := matcher.getAppNumArgs, numDiscrs := numDiscrs, altNumParams := minors.map Prod.snd, uElimPos? := uElimPos? }
     setInlineAttribute matcherName
     trace[Meta.Match.debug]! "matcher: {matcher}"

src/Lean/Meta/RecursorInfo.lean

@@ -270,8 +270,7 @@ builtin_initialize recursorAttribute : ParametricAttribute Nat ←
     descr := "user defined recursor, numerical parameter specifies position of the major premise",
     getParam := fun _ stx => ofExcept $ syntaxToMajorPos stx,
     afterSet := fun declName majorPos => do
-      (mkRecursorInfoCore declName (some majorPos)).run'
-      pure ()
+      discard <| mkRecursorInfoCore declName (some majorPos) |>.run'
   }
 
 def getMajorPos? (env : Environment) (declName : Name) : Option Nat :=

src/Lean/Meta/UnificationHint.lean

@@ -85,8 +85,7 @@ builtin_initialize
     descr := "unification hint"
     add   := fun declName args kind => do
       if args.hasArgs then throwError "invalid attribute 'unificationHint', unexpected argument"
-      addUnificationHint declName kind |>.run
-      pure ()
+      discard <| addUnificationHint declName kind |>.run
   }
 
 def tryUnificationHints (t s : Expr) : MetaM Bool := do

src/Lean/Parser/Extension.lean

@@ -376,8 +376,8 @@ def categoryParserFnImpl (catName : Name) : ParserFn := fun ctx s =>
 def addToken (env : Environment) (tk : Token) : Except String Environment := do
   -- Recall that `ParserExtension.addEntry` is pure, and assumes `addTokenConfig` does not fail.
   -- So, we must run it here to handle exception.
-  addTokenConfig (parserExtension.getState env).tokens tk
-  pure $ parserExtension.addEntry env <| ParserExtension.Entry.token tk
+  discard <| addTokenConfig (parserExtension.getState env).tokens tk
+  return parserExtension.addEntry env <| ParserExtension.Entry.token tk
 
 def addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment :=
   parserExtension.addEntry env <| ParserExtension.Entry.kind k

src/Lean/ParserCompiler/Attribute.lean

@@ -31,7 +31,7 @@ def registerCombinatorAttribute (name : Name) (descr : String)
       let env ← getEnv
       match attrParamSyntaxToIdentifier args with
       | some parserDeclName => do
-        getConstInfo parserDeclName
+        discard <| getConstInfo parserDeclName
         setEnv <| ext.addEntry env (parserDeclName, decl)
       | none            => throwError! "invalid [{name}] argument, expected identifier"
   }

src/Lean/Server.lean

@@ -229,7 +229,7 @@ def initAndRunServer (i o : FS.Stream) : IO Unit := do
       { capabilities := mkLeanServerCapabilities,
         serverInfo? := some { name := "Lean 4 server",
                               version? := "0.0.1" } : InitializeResult }
-    readLspNotificationAs "initialized" InitializedParams
+    discard <| readLspNotificationAs "initialized" InitializedParams
     mainLoop ()
     let Message.notification "exit" none ← readLspMessage
       | throw (userError "Expected an Exit Notification.")