feat: explicit defeq attribute (#8419)

This PR introduces an explicit `defeq` attribute to mark theorems that
can be used by `dsimp`. The benefit of an explicit attribute over the
prior logic of looking at the proof body is that we can reliably omit
theorem bodies across module boundaries. It also helps with intra-file
parallelism.

If a theorem is syntactically defined by `:= rfl`, then the attribute is
assumed and need not given explicitly. This is a purely syntactic check
and can be fooled, e.g. if in the current namespace, `rfl` is not
actually “the” `rfl` of `Eq`. In that case, some other syntax has be
used, such as `:= (rfl)`. This is also the way to go if a theorem can be
proved by `defeq`, but one does not actually want `dsimp` to use this
fact.

The `defeq` attribute will look at the *type* of the declaration, not
the body, to check if it really holds definitionally. Because of
different reduction settings, this can sometimes go wrong. Then one
should also write `:= (rfl)`, if one does not want this to be a defeq
theorem. (If one does then this is currently not possible, but it’s
probably a bad idea anyways).

The `set_option debug.tactic.simp.checkDefEqAttr true`, `dsimp` will
warn if could not apply a lemma due to a missing `defeq` attribute.

With `set_option backward.dsimp.useDefEqAttr.get false` one can revert
to the old behavior of inferring rfl-ness based on the theorem body.

Both options will go away eventually (too bad we can’t mark them as
deprecated right away, see #7969)

Meta programs that generate theorems (e.g. equational theorems) can use
`inferDefEqAttr` to set the attribute based on the theorem body of the
just created declaration.

This builds on #8501 to update Init to `@[expose]` a fair amount of
definitions that, if not exposed, would prevent some existing `:= rfl`
theorems from being `defeq` theorems. In the interest of starting
backwards compatible, I exposed these function. Hopefully many can be
un-exposed later again.

A mathlib adaption branch exists that includes both the meta programming
fixes and changes to the theorems (e.g. changing `:= by rfl` to `:=
rfl`).

With the module system there is now no special handling for `defeq`
theorem bodies, because we don’t look at the body anymore. The previous
hack is removed. The `defeq`-ness of the theorem needs to be checked in
the context of the theorem’s *type*; the error message contains a hint
if the defeq check fails because of the exported context.

src/Init/Data/Fin/Fold.lean

@@ -183,10 +183,7 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
   | zero =>
     rw [foldrM_loop_zero, foldrM_loop_succ, pure_bind]
     conv => rhs; rw [←bind_pure (f 0 x)]
-    congr
-    try  -- TODO: block can be deleted after bootstrapping
-      funext
-      simp [foldrM_loop_zero]
+    rfl
   | succ i ih =>
     rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
     congr; funext; exact ih ..

src/Lean.lean

@@ -41,3 +41,4 @@ import Lean.PrivateName
 import Lean.PremiseSelection
 import Lean.Namespace
 import Lean.EnvExtension
+import Lean.DefEqAttrib

src/Lean/AddDecl.lean

@@ -64,13 +64,6 @@ Checks whether the declaration was originally declared as a theorem; see also
 def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool :=
   getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false
 
--- HACK: remove together with MutualDef HACK when `[dsimp]` is introduced
-private def isSimpleRflProof (proof : Expr) : Bool :=
-  if let .lam _ _ proof _ := proof then
-    isSimpleRflProof proof
-  else
-    proof.isAppOfArity ``rfl 2
-
 private def looksLikeRelevantTheoremProofType (type : Expr) : Bool :=
   if let .forallE _ _ type _ := type then
     looksLikeRelevantTheoremProofType type
@@ -90,9 +83,6 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   let (name, info, kind) ← match decl with
     | .thmDecl thm =>
       let exportProof := !(← getEnv).header.isModule ||
-        -- We should preserve rfl theorems but also we should not override a decision to hide by the
-        -- MutualDef elaborator via `withoutExporting`
-        (← getEnv).isExporting && isSimpleRflProof thm.value ||
         -- TODO: this is horrible...
         looksLikeRelevantTheoremProofType thm.type
       if !exportProof then

src/Lean/Attributes.lean

@@ -135,7 +135,9 @@ structure TagAttribute where
   deriving Inhabited
 
 def registerTagAttribute (name : Name) (descr : String)
-    (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%) (applicationTime := AttributeApplicationTime.afterTypeChecking) : IO TagAttribute := do
+    (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%)
+    (applicationTime := AttributeApplicationTime.afterTypeChecking)
+    (asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO TagAttribute := do
   let ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension {
     name            := ref
     mkInitial       := pure {}
@@ -145,6 +147,12 @@ def registerTagAttribute (name : Name) (descr : String)
       let r : Array Name := es.fold (fun a e => a.push e) #[]
       r.qsort Name.quickLt
     statsFn         := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
+    asyncMode       := asyncMode
+    replay?         := some fun _ newState newConsts s =>
+      newConsts.foldl (init := s) fun s c =>
+        if newState.contains c then
+          s.insert c
+        else s
   }
   let attrImpl : AttributeImpl := {
     ref, name, descr, applicationTime
@@ -153,7 +161,9 @@ def registerTagAttribute (name : Name) (descr : String)
       unless kind == AttributeKind.global do throwError "invalid attribute '{name}', must be global"
       let env ← getEnv
       unless (env.getModuleIdxFor? decl).isNone do
-        throwError "invalid attribute '{name}', declaration is in an imported module"
+        throwError "invalid attribute '{name}', declaration {.ofConstName decl} is in an imported module"
+      unless env.asyncMayContain decl do
+        throwError "invalid attribute '{name}', declaration {.ofConstName decl} is not from the present async context {env.asyncPrefix?}"
       validate decl
       modifyEnv fun env => ext.addEntry env decl
   }
@@ -162,10 +172,27 @@ def registerTagAttribute (name : Name) (descr : String)
 
 namespace TagAttribute
 
+/-- Sets the attribute (without running `validate`) -/
+def setTag  [Monad m] [MonadError m] [MonadEnv m] (attr : TagAttribute) (decl : Name) : m Unit := do
+  let env ← getEnv
+  unless (env.getModuleIdxFor? decl).isNone do
+    throwError "invalid attribute '{attr.attr.name}', declaration {.ofConstName decl} is in an imported module"
+  unless env.asyncMayContain decl do
+    throwError "invalid attribute '{attr.attr.name}', declaration {.ofConstName decl} is not from the present async context {env.asyncPrefix?}"
+  modifyEnv fun env => attr.ext.addEntry env decl
+
 def hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool :=
   match env.getModuleIdxFor? decl with
   | some modIdx => (attr.ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt
-  | none        => (attr.ext.getState env).contains decl
+  | none        =>
+    if attr.ext.toEnvExtension.asyncMode matches .async then
+      -- It seems that the env extension API doesn't quite allow querying attributes in a way
+      -- that works for realizable constants, but without waiting on proofs to finish.
+      -- Until then, we use the following overapproximation, to be refined later:
+      (attr.ext.findStateAsync env decl).contains decl ||
+      (attr.ext.getState env (asyncMode := .local)).contains decl
+    else
+      (attr.ext.getState env).contains decl
 
 end TagAttribute
 

src/Lean/Declaration.lean

@@ -482,7 +482,7 @@ def value! (info : ConstantInfo) (allowOpaque := false) : Expr :=
   | .defnInfo {value, ..}   => value
   | .thmInfo  {value, ..}   => value
   | .opaqueInfo {value, ..} => if allowOpaque then value else panic! "declaration with value expected"
-  | _                       => panic! "declaration with value expected"
+  | _                       => panic! s!"declaration with value expected, but {info.name} has none"
 
 def hints : ConstantInfo → ReducibilityHints
   | .defnInfo {hints, ..} => hints

src/Lean/DefEqAttrib.lean

@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+
+import Lean.PrettyPrinter
+
+namespace Lean
+open Meta
+
+/--
+There are defeq theorems that only hold at transparency `.all`, but also others that hold
+(from the kernel's point of view) but where the defeq checker here will run out of cycles.
+
+So we try the more careful first.
+-/
+private def isDefEqCareful (e1 e2 : Expr) : MetaM Bool := do
+  withOptions (smartUnfolding.set · false) <| do
+    withDefault (isDefEq e1 e2) <||> withTransparency .all (isDefEq e1 e2)
+
+def validateDefEqAttr (declName : Name) : AttrM Unit := do
+  let info ← getConstVal declName
+  MetaM.run' do
+    withTransparency .all do -- we want to look through defs in `info.type` all the way to `Eq`
+      forallTelescopeReducing info.type fun _ type => do
+        let type ← whnf type
+        -- NB: The warning wording should work both for explicit uses of `@[defeq]` as well as the implicit `:= rfl`.
+        let some (_, lhs, rhs) := type.eq? |
+          throwError m!"Not a definitional equality: the conclusion should be an equality, but is{inlineExpr type}"
+        let ok ← isDefEqCareful lhs rhs
+        unless ok do
+          let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
+            let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
+            let mut msg := m!"Not a definitional equality: the left-hand side{indentExpr lhs}\nis \
+              not definitionally equal to the right-hand side{indentExpr rhs}"
+            if (← getEnv).isExporting then
+              let okPrivately ← withoutExporting <| isDefEqCareful lhs rhs
+              if okPrivately then
+                msg := msg ++ .note m!"This theorem is exported from the current module. \
+                  This requires that all definitions that need to be unfolded to prove this \
+                  theorem must be exposed."
+            pure msg
+          throwError explanation
+
+/--
+Marks the theorem as a definitional equality.
+
+The theorem must be an equality that holds by `rfl`. This allows `dsimp` to use this theorem
+when rewriting.
+
+A theorem with with a definition that is (syntactically) `:= rfl` is implicitly marked `@[defeq]`.
+To avoid this behavior, write `:= (rfl)` instead.
+
+The attribute should be given before a `@[simp]` attribute to have effect.
+
+When using the module system, an exported theorem can only be `@[defeq]` if all definitions that
+need to be unfolded to prove the theorem are exported and exposed.
+-/
+@[builtin_doc]
+builtin_initialize defeqAttr : TagAttribute ←
+  registerTagAttribute `defeq "mark theorem as a definitional equality, to be used by `dsimp`"
+    (validate := validateDefEqAttr) (applicationTime := .afterTypeChecking)
+    (asyncMode := .async)
+
+private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
+  match type with
+  | .forallE _ _ type _ =>
+    if let .lam _ _ proof _ := proof then
+      isRflProofCore type proof
+    else
+      return false
+  | _ =>
+    if type.isAppOfArity ``Eq 3 then
+      if proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2 then
+        return true
+      else if proof.isAppOfArity ``Eq.symm 4 then
+        -- `Eq.symm` of rfl proof is a rfl proof
+        isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type
+      else if proof.getAppFn.isConst then
+        -- The application of a `defeq` theorem is a `rfl` proof
+        return defeqAttr.hasTag (← getEnv) proof.getAppFn.constName!
+      else
+        return false
+    else
+      return false
+
+/--
+For automatically generated theorems (equational theorems etc.), we want to set the `defeq` attribute
+if the proof is `rfl`, essentially reproducing the behavior before the introduction of the `defeq`
+attribute. This function infers the `defeq` attribute based on the declaration value.
+-/
+def inferDefEqAttr (declName : Name) : MetaM Unit := do
+  withoutExporting do
+    let info ← getConstInfo declName
+    let isRfl ←
+      if let some value := info.value? then
+        isRflProofCore info.type value
+      else
+        pure false
+    if isRfl then
+      try
+        withExporting (isExporting := !isPrivateName declName) do
+          validateDefEqAttr declName -- sanity-check: would we have accepted `@[defeq]` on this?
+      catch e =>
+        logError m!"Theorem {declName} has a `rfl`-proof and was thus inferred to be `@[defeq]`, \
+          but validating that attribute failed:{indentD e.toMessageData}"
+      defeqAttr.setTag declName

src/Lean/Elab/DeclModifiers.lean

@@ -84,10 +84,14 @@ def Modifiers.isNonrec : Modifiers → Bool
   | { recKind := .nonrec, .. } => true
   | _                          => false
 
-/-- Adds attribute `attr` in `modifiers` -/
+/-- Adds attribute `attr` in `modifiers`, at the end -/
 def Modifiers.addAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
   { modifiers with attrs := modifiers.attrs.push attr }
 
+/-- Adds attribute `attr` in `modifiers`, at the beginning -/
+def Modifiers.addFirstAttr (modifiers : Modifiers) (attr : Attribute) : Modifiers :=
+  { modifiers with attrs := #[attr] ++ modifiers.attrs }
+
 /-- Filters attributes using `p` -/
 def Modifiers.filterAttrs (modifiers : Modifiers) (p : Attribute → Bool) : Modifiers :=
   { modifiers with attrs := modifiers.attrs.filter p }

src/Lean/Elab/DefView.lean

@@ -127,6 +127,11 @@ structure DefView where
 def DefView.isInstance (view : DefView) : Bool :=
   view.modifiers.attrs.any fun attr => attr.name == `instance
 
+/-- Prepends the `defeq` attribute, removing existing ones if there are any -/
+def DefView.markDefEq (view : DefView) : DefView :=
+  { view with modifiers :=
+      view.modifiers.filterAttrs (·.name != `defeq) |>.addFirstAttr { name := `defeq } }
+
 namespace Command
 open Meta
 

src/Lean/Elab/MutualDef.lean

@@ -1072,34 +1072,20 @@ where
     withExporting (isExporting := !expandedDeclIds.all (isPrivateName ·.declName)) do
     let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises
     let headers ← levelMVarToParamHeaders views headers
-    -- If the decl looks like a `rfl` theorem, we elaborate is synchronously as we need to wait for
-    -- the type before we can decide whether the theorem body should be exported and then waiting
-    -- for the body as well should not add any significant overhead.
-    let isRflLike := headers.all (·.value matches `(declVal| := rfl))
-    -- elaborate body in parallel when all stars align
     if let (#[view], #[declId]) := (views, expandedDeclIds) then
-      if Elab.async.get (← getOptions) && view.kind.isTheorem && !isRflLike &&
+      if Elab.async.get (← getOptions) && view.kind.isTheorem &&
           !deprecated.oldSectionVars.get (← getOptions) &&
           -- holes in theorem types is not a fatal error, but it does make parallelism impossible
           !headers[0]!.type.hasMVar then
         elabAsync headers[0]! view declId
-      else elabSync headers isRflLike
-    else elabSync headers isRflLike
+      else elabSync headers
+    else elabSync headers
     for view in views, declId in expandedDeclIds do
       -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting
       -- that depends only on a part of the ref
       addDeclarationRangesForBuiltin declId.declName view.modifiers.stx view.ref
-  elabSync headers isRflLike := do
-    -- If the reflexivity holds publicly as well (we're still inside `withExporting` here), export
-    -- the body even if it is a theorem so that it is recognized as a rfl theorem even without
-    -- `import all`.
-    let rflPublic ← pure isRflLike <&&> pure (← getEnv).header.isModule <&&>
-      forallTelescopeReducing headers[0]!.type fun _ type => do
-        let some (_, lhs, rhs) := type.eq? | pure false
-        try
-          isDefEq lhs rhs
-        catch _ => pure false
-    finishElab (isExporting := rflPublic) headers
+  elabSync headers := do
+    finishElab headers
     processDeriving headers
   elabAsync header view declId := do
     let env ← getEnv
@@ -1147,7 +1133,7 @@ where
         (cancelTk? := cancelTk) fun _ => do profileitM Exception "elaboration" (← getOptions) do
       setEnv async.asyncEnv
       try
-        finishElab (isExporting := false) #[header]
+        finishElab #[header]
       finally
         reportDiag
         -- must introduce node to fill `infoHole` with multiple info trees
@@ -1279,6 +1265,8 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
     if ds.size > 1 && modifiers.isNonrec then
       throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
     let mut view ← mkDefView modifiers d[1]
+    if view.kind != .example && view.value matches `(declVal| := rfl) then
+      view := view.markDefEq
     let fullHeaderRef := mkNullNode #[d[0], view.headerRef]
     if let some snap := snap? then
       view := { view with headerSnap? := some {

src/Lean/Elab/PreDefinition/EqUnfold.lean

@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Rfl
 import Lean.Meta.Tactic.Intro
 import Lean.Meta.Tactic.Apply
+import Lean.DefEqAttrib
 
 namespace Lean.Meta
 
@@ -53,6 +54,7 @@ def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
       name, type, value
       levelParams := info.levelParams
     }
+    inferDefEqAttr name
   return some name
 
 

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -12,6 +12,7 @@ import Lean.Meta.Tactic.Split
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Refl
 import Lean.Meta.Match.MatchEqs
+import Lean.DefEqAttrib
 
 namespace Lean.Elab.Eqns
 open Meta
@@ -429,6 +430,7 @@ where
       name, type, value
       levelParams := info.levelParams
     }
+    inferDefEqAttr name
 
 /--
   Auxiliary method for `mkUnfoldEq`. The structure is based on `mkEqnTypes`.

src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -36,6 +36,7 @@ where
         name, type, value
         levelParams := info.levelParams
       }
+      inferDefEqAttr name
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if (← isRecursiveDefinition declName) then

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -26,40 +26,51 @@ structure EqnInfo extends EqnInfoCore where
   deriving Inhabited
 
 private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
-  trace[Elab.definition.structural.eqns] "proving: {type}"
-  withNewMCtxDepth do
-    let main ← mkFreshExprSyntheticOpaqueMVar type
-    let (_, mvarId) ← main.mvarId!.intros
-    unless (← tryURefl mvarId) do -- catch easy cases
-      go (← deltaLHS mvarId)
-    instantiateMVars main
+  withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} proving:{indentExpr type}") do
+    withNewMCtxDepth do
+      let main ← mkFreshExprSyntheticOpaqueMVar type
+      let (_, mvarId) ← main.mvarId!.intros
+      unless (← tryURefl mvarId) do -- catch easy cases
+        go (← deltaLHS mvarId)
+      instantiateMVars main
 where
   go (mvarId : MVarId) : MetaM Unit := do
-    trace[Elab.definition.structural.eqns] "step\n{MessageData.ofGoal mvarId}"
-    if (← tryURefl mvarId) then
-      return ()
-    else if (← tryContradiction mvarId) then
-      return ()
-    else if let some mvarId ← whnfReducibleLHS? mvarId then
-      go mvarId
-    else if let some mvarId ← simpMatch? mvarId then
-      go mvarId
-    else if let some mvarId ← simpIf? mvarId then
-      go mvarId
-    else
-      let ctx ← Simp.mkContext
-      match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
-      | TacticResultCNM.closed => return ()
-      | TacticResultCNM.modified mvarId => go mvarId
-      | TacticResultCNM.noChange =>
-        if let some mvarId ← deltaRHS? mvarId declName then
+    withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} step:\n{MessageData.ofGoal mvarId}") do
+      if (← tryURefl mvarId) then
+        trace[Elab.definition.structural.eqns] "tryURefl succeeded"
+        return ()
+      else if (← tryContradiction mvarId) then
+        trace[Elab.definition.structural.eqns] "tryContadiction succeeded"
+        return ()
+      else if let some mvarId ← whnfReducibleLHS? mvarId then
+        trace[Elab.definition.structural.eqns] "whnfReducibleLHS succeeded"
+        go mvarId
+      else if let some mvarId ← simpMatch? mvarId then
+        trace[Elab.definition.structural.eqns] "simpMatch? succeeded"
+        go mvarId
+      else if let some mvarId ← simpIf? mvarId then
+        trace[Elab.definition.structural.eqns] "simpIf? succeeded"
+        go mvarId
+      else
+        let ctx ← Simp.mkContext
+        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
+        | TacticResultCNM.closed =>
+          trace[Elab.definition.structural.eqns] "simpTargetStar closed the goal"
+        | TacticResultCNM.modified mvarId =>
+          trace[Elab.definition.structural.eqns] "simpTargetStar modified the goal"
           go mvarId
-        else if let some mvarIds ← casesOnStuckLHS? mvarId then
-          mvarIds.forM go
-        else if let some mvarIds ← splitTarget? mvarId then
-          mvarIds.forM go
-        else
-          throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
+        | TacticResultCNM.noChange =>
+          if let some mvarId ← deltaRHS? mvarId declName then
+            trace[Elab.definition.structural.eqns] "deltaRHS? succeeded"
+            go mvarId
+          else if let some mvarIds ← casesOnStuckLHS? mvarId then
+            trace[Elab.definition.structural.eqns] "casesOnStuckLHS? succeeded"
+            mvarIds.forM go
+          else if let some mvarIds ← splitTarget? mvarId then
+            trace[Elab.definition.structural.eqns] "splitTarget? succeeded"
+            mvarIds.forM go
+          else
+            throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
 
 def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
   withOptions (tactic.hygienic.set · false) do
@@ -71,7 +82,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
   let mut thmNames := #[]
   for h : i in [: eqnTypes.size] do
     let type := eqnTypes[i]
-    trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
+    trace[Elab.definition.structural.eqns] "eqnType {i+1}: {type}"
     let name := mkEqLikeNameFor (← getEnv) info.declName s!"{eqnThmSuffixBasePrefix}{i+1}"
     thmNames := thmNames.push name
     -- determinism: `type` should be independent of the environment changes since `baseName` was
@@ -86,6 +97,7 @@ where
       name, type, value
       levelParams := info.levelParams
     }
+    inferDefEqAttr name
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
@@ -119,6 +131,7 @@ where
         name, type, value
         levelParams := info.levelParams
       }
+      inferDefEqAttr name
 
 def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/PreDefinition/WF/Unfold.lean

@@ -96,6 +96,7 @@ def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessPr
         name, type, value
         levelParams := preDef.levelParams
       }
+      inferDefEqAttr name
       trace[Elab.definition.wf] "mkUnfoldEq defined {.ofConstName name}"
 
 /--
@@ -127,6 +128,7 @@ def mkBinaryUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM U
         name, type, value
         levelParams := preDef.levelParams
       }
+      inferDefEqAttr name
       trace[Elab.definition.wf] "mkBinaryUnfoldEq defined {.ofConstName name}"
 
 builtin_initialize

src/Lean/Elab/Print.lean

@@ -29,6 +29,9 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
   | ReducibilityStatus.reducible =>     attrs := attrs.push m!"reducible"
   | ReducibilityStatus.semireducible => pure ()
 
+  if defeqAttr.hasTag (← getEnv) id then
+    attrs := attrs.push m!"defeq"
+
   let mut m : MessageData := m!""
   unless attrs.isEmpty do
     m := m ++ "@[" ++ MessageData.joinSep attrs.toList ", " ++ "] "

src/Lean/Meta/Eqns.lean

@@ -9,6 +9,7 @@ import Lean.AddDecl
 import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 import Lean.Meta.Match.MatcherInfo
+import Lean.DefEqAttrib
 
 namespace Lean.Meta
 
@@ -182,6 +183,7 @@ where doRealize name info := do
       name, type, value
       levelParams := info.levelParams
     }
+    inferDefEqAttr name -- should always succeed
 
 /--
 Returns `some declName` if `thmName` is an equational theorem for `declName`.

src/Lean/Meta/SizeOf.lean

@@ -8,6 +8,7 @@ import Init.Data.List.BasicAux
 import Lean.AddDecl
 import Lean.Meta.AppBuilder
 import Lean.Meta.Instances
+import Lean.DefEqAttrib
 
 namespace Lean.Meta
 
@@ -148,14 +149,16 @@ partial def mkSizeOfFn (recName : Name) (declName : Name): MetaM Unit := do
           trace[Meta.sizeOf] "declName: {declName}"
           trace[Meta.sizeOf] "type: {sizeOfType}"
           trace[Meta.sizeOf] "val: {sizeOfValue}"
-          addDecl <| Declaration.defnDecl {
-            name        := declName
-            levelParams := levelParams
-            type        := sizeOfType
-            value       := sizeOfValue
-            safety      := DefinitionSafety.safe
-            hints       := ReducibilityHints.abbrev
-          }
+          -- We expose the `sizeOf` functions so that the `spec` theorems can be publicly `defeq`
+          withExporting do
+            addDecl <| Declaration.defnDecl {
+              name        := declName
+              levelParams := levelParams
+              type        := sizeOfType
+              value       := sizeOfValue
+              safety      := DefinitionSafety.safe
+              hints       := ReducibilityHints.abbrev
+            }
 
 /--
   Create `sizeOf` functions for all inductive datatypes in the mutual inductive declaration containing `typeName`
@@ -457,6 +460,7 @@ private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name
         type        := thmType
         value       := thmValue
       }
+      inferDefEqAttr thmName
       simpAttr.add thmName default AttributeKind.global
 
 private def mkSizeOfSpecTheorems (indTypeNames : Array Name) (sizeOfFns : Array Name) (recMap : NameMap Name) : MetaM Unit := do
@@ -500,14 +504,16 @@ def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
                   let instDeclType ← mkForallFVars (xs ++ localInsts) sizeOfIndType
                   let instDeclValue ← mkLambdaFVars (xs ++ localInsts) sizeOfMk
                   trace[Meta.sizeOf] ">> {instDeclName} : {instDeclType}"
-                  addDecl <| Declaration.defnDecl {
-                    name        := instDeclName
-                    levelParams := indInfo.levelParams
-                    type        := instDeclType
-                    value       := instDeclValue
-                    safety      := .safe
-                    hints       := .abbrev
-                  }
+                  -- We expose the `sizeOf` instance so that the `spec` theorems can be publicly `defeq`
+                  withExporting do
+                    addDecl <| Declaration.defnDecl {
+                      name        := instDeclName
+                      levelParams := indInfo.levelParams
+                      type        := instDeclType
+                      value       := instDeclValue
+                      safety      := .safe
+                      hints       := .abbrev
+                    }
                   addInstance instDeclName AttributeKind.global (eval_prio default)
         if genSizeOfSpec.get (← getOptions) then
           mkSizeOfSpecTheorems indInfo.all.toArray fns recMap

src/Lean/Meta/Tactic/AuxLemma.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.AddDecl
 import Lean.Meta.Basic
+import Lean.DefEqAttrib
 
 namespace Lean.Meta
 
@@ -27,7 +28,8 @@ builtin_initialize auxLemmasExt : EnvExtension AuxLemmas ←
   This method is useful for tactics (e.g., `simp`) that may perform preprocessing steps to lemmas provided by
   users. For example, `simp` preprocessor may convert a lemma into multiple ones.
 -/
-def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : Option Name := none) (cache := true) : MetaM Name := do
+def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : Option Name := none)
+    (cache := true) (inferRfl := false) : MetaM Name := do
   let env ← getEnv
   let s := auxLemmasExt.getState env
   let mkNewAuxLemma := do
@@ -47,6 +49,8 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) (kind? : O
           levelParams, type, value
         }
     addDecl decl
+    if inferRfl then
+      inferDefEqAttr auxName
     modifyEnv fun env => auxLemmasExt.modifyState env fun ⟨lemmas⟩ => ⟨lemmas.insert type (auxName, levelParams)⟩
     return auxName
   if cache then

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

@@ -110,7 +110,7 @@ where
       return false
 
 private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
-  if thm.isRfl (← getEnv) then
+  if thm.rfl then
     return (← getConfig).implicitDefEqProofs
   else
     return false
@@ -218,10 +218,19 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
       for (thm, numExtraArgs) in candidates do
-        unless inErasedSet thm || (rflOnly && !thm.isRfl (← getEnv)) do
-          if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
-            trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
-            return some result
+        if inErasedSet thm then continue
+        if rflOnly then
+          unless thm.rfl do
+            if debug.tactic.simp.checkDefEqAttr.get (← getOptions) &&
+               backward.dsimp.useDefEqAttr.get (← getOptions) then
+              let isRflOld ← withOptions (backward.dsimp.useDefEqAttr.set · false) do
+                isRflProof thm.proof
+              if isRflOld then
+                logWarning m!"theorem {thm.proof} is no longer rfl"
+            continue
+        if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
+          trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
+          return some result
       return none
 
   /--
@@ -236,7 +245,7 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority
       for thm in candidates do
-        unless inErasedSet thm || (rflOnly && !thm.isRfl (← getEnv)) do
+        unless inErasedSet thm || (rflOnly && !thm.rfl) do
           let result? ← withNewMCtxDepth do
             let val  ← thm.getValue
             let type ← inferType val

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

@@ -10,10 +10,23 @@ import Lean.Meta.DiscrTree
 import Lean.Meta.AppBuilder
 import Lean.Meta.Eqns
 import Lean.Meta.Tactic.AuxLemma
+import Lean.DefEqAttrib
 import Lean.DocString
-import Lean.PrettyPrinter
 namespace Lean.Meta
 
+register_builtin_option backward.dsimp.useDefEqAttr : Bool := {
+  defValue := true
+  descr    := "Use `defeq` attribute rather than checking theorem body to decide whether a theroem \
+    can be used in `dsimp` or with `implicitDefEqProofs`."
+}
+
+register_builtin_option debug.tactic.simp.checkDefEqAttr : Bool := {
+  defValue := false
+  descr    := "If true, whenever `dsimp` fails to apply a rewrite rule because it is not marked as \
+    `defeq`, check whether it would have been considered as a rfl theorem before the introduction \
+    of the `defeq` attribute, and warn if it was. Note that this is a costly check."
+}
+
 /--
 An `Origin` is an identifier for simp theorems which indicates roughly
 what action the user took which lead to this theorem existing in the simp set.
@@ -123,23 +136,11 @@ structure SimpTheorem where
   -/
   origin      : Origin
   /--
-  `rfl` is true if `proof` is by `Eq.refl` or `rfl`.
-
-  NOTE: As the visibility of `proof` may have changed between the point of declaration and use
-  of a `@[simp]` theorem, `isRfl` must be used to check for this flag.
+  `rfl` is true if `proof` is by `Eq.refl`, `rfl` or a `@[defeq]` theorem.
   -/
   rfl         : Bool
   deriving Inhabited
 
-/-- Checks whether the theorem holds by reflexivity in the scope given by the environment. -/
-def SimpTheorem.isRfl (s : SimpTheorem) (env : Environment) : Bool := Id.run do
-  if !s.rfl then
-    return false
-  let .decl declName _ _ := s.origin |
-    return true  -- not a global simp theorem, proof visibility must be unchanged
-  -- If we can see the proof, it must hold in the current scope.
-  env.findAsync? declName matches some ({ kind := .thm, .. })
-
 mutual
   private partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
     match type with
@@ -165,9 +166,12 @@ mutual
         return false
 
   private partial def isRflTheoremCore (declName : Name) : CoreM Bool := do
-    let { kind := .thm, constInfo, .. } ← getAsyncConstInfo declName | return false
-    let .thmInfo info ← traceBlock "isRflTheorem theorem body" constInfo | return false
-    isRflProofCore info.type info.value
+    if backward.dsimp.useDefEqAttr.get (← getOptions) then
+      return defeqAttr.hasTag (← getEnv) declName
+    else
+      let { kind := .thm, constInfo, .. } ← getAsyncConstInfo declName | return false
+      let .thmInfo info ← traceBlock "isRflTheorem theorem body" constInfo | return false
+      isRflProofCore info.type info.value
 end
 
 def isRflTheorem (declName : Name) : CoreM Bool :=
@@ -439,7 +443,7 @@ private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool)
     if inv || (← shouldPreprocess type) then
       let mut r := #[]
       for (val, type) in (← preprocess val type inv (isGlobal := true)) do
-        let auxName ← mkAuxLemma (kind? := `_simp) cinfo.levelParams type val
+        let auxName ← mkAuxLemma (kind? := `_simp) cinfo.levelParams type val (inferRfl := true)
         r := r.push <| (← withoutExporting do mkSimpTheoremCore origin (mkConst auxName us) #[] (mkConst auxName) post prio (noIndexAtArgs := false))
       return r
     else

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/1081.lean

@@ -20,7 +20,7 @@ namespace Vector'
   | ⟨i+1, h⟩, cons x xs => cons x $ xs.insert a ⟨i, Nat.lt_of_succ_lt_succ h⟩
 
   theorem insert_at_0_eq_cons1 (a: α) (v: Vector' α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v :=
-    rfl -- Error, it does not hold by reflexivity because the recursion is on v
+    (rfl) -- Error, it does not hold by reflexivity because the recursion is on v
 
   example (a : α) :  nil.insert a ⟨0, by simp +arith⟩ = cons a nil :=
     rfl

tests/lean/1081.lean.expected.out

@@ -4,7 +4,7 @@ has type
   ?m = ?m : Prop
 but is expected to have type
   f 0 y = y : Prop
-1081.lean:23:4-23:7: error: type mismatch
+1081.lean:23:4-23:9: error: type mismatch
   rfl
 has type
   ?m = ?m : Prop

tests/lean/1113.lean

@@ -2,15 +2,19 @@ def foo: {n: Nat} → Fin n → Nat
 |   0, _ => 0
 | n+1, _ => 0
 
+-- Local copy to make test more robust against staging issues
+@[simp] theorem Nat.succ_eq_add_one' (n : Nat) : succ n = n + 1 :=
+  rfl
+
 theorem t3 {f: Fin (n+1)}:
   foo f = 0 := by
-  dsimp only [←Nat.succ_eq_add_one n] at f -- use `dsimp` to ensure we don't copy `f`
+  dsimp only [←Nat.succ_eq_add_one' n] at f -- use `dsimp` to ensure we don't copy `f`
   trace_state
-  simp only [←Nat.succ_eq_add_one n, foo]
+  simp only [←Nat.succ_eq_add_one' n, foo]
 
 example {n: Nat} {f: Fin (n+1)}:
   foo f = 0 := by
   revert f
-  rw[←Nat.succ_eq_add_one n]
+  rw[←Nat.succ_eq_add_one' n]
   intro f
   simp only [foo]

tests/lean/1433.lean

@@ -8,7 +8,7 @@ def wrongRem := 1
 theorem correct₁ : dividend / divisor = correctQuot := rfl
 theorem correct₂ : dividend = divisor * correctQuot + correctRem := rfl
 
-theorem wrong : dividend % divisor = wrongRem := rfl
+theorem wrong : dividend % divisor = wrongRem := (rfl)
 
 theorem unsound : False := by
   have : wrongRem = correctRem := by

tests/lean/1433.lean.expected.out

@@ -1,4 +1,4 @@
-1433.lean:11:49-11:52: error: type mismatch
+1433.lean:11:49-11:54: error: type mismatch
   rfl
 has type
   ?m = ?m : Prop

tests/lean/dsimpViaConst.lean

@@ -36,7 +36,7 @@ def w : Bool → Bool | b => b
 example : w true = true := by dsimp
 
 theorem foo_internal_with_arg (_ : Nat) : w true = true := rfl
-@[simp] theorem foo_using_arg : w true = true := foo_internal_with_arg 0
+@[simp, defeq] theorem foo_using_arg : w true = true := foo_internal_with_arg 0
 
 example : w true = true := by dsimp
 
@@ -47,6 +47,6 @@ example : w true = true := by dsimp
 example : w false = false := by dsimp
 
 theorem foo_internal_without_arg : w false = false := rfl
-@[simp] theorem foo_without_arg : w false = false := foo_internal_without_arg
+@[simp, defeq] theorem foo_without_arg : w false = false := foo_internal_without_arg
 
 example : w false = false := by dsimp

tests/lean/etaStructIssue.lean

@@ -17,4 +17,4 @@ def mkNat (e : E) (x : F e) : Nat :=
 theorem fail (e : E) (x₁ : F e) (x₂ : F (E.mk e)) : mkNat e x₁ = mkNat (E.mk e) x₂ :=
   /- The following rfl was succeeding in the elaborator but failing in the kernel because
      of a discrepancy in the implementation for Eta-for-structures. -/
-  rfl -- should fail
+  (rfl) -- should fail

tests/lean/etaStructIssue.lean.expected.out

@@ -1,4 +1,4 @@
-etaStructIssue.lean:20:2-20:5: error: type mismatch
+etaStructIssue.lean:20:2-20:7: error: type mismatch
   rfl
 has type
   ?m = ?m : Prop

tests/lean/interactive/isRflParallel.lean

@@ -0,0 +1,42 @@
+import Lean.Server.Test.Cancel
+
+open Lean Meta
+
+/-!
+The following should not deadlock: The `simp` tactic should be able to use `a_eq_b` even before
+that theorem body is evaluated.
+
+TODO: Does't work any more with the rfl extension being .async, as that waits for the body to be
+evaluated.
+-/
+
+-- set_option trace.Elab.block true
+set_option debug.skipKernelTC true
+set_option backward.dsimp.useDefEqAttr false
+set_option debug.tactic.simp.checkDefEqAttr false
+
+axiom testSorry : α
+
+opaque a : Nat
+opaque b : Nat
+
+theorem a_eq_b : a = b := by
+  -- Three possible ways to pretend this theorem takes a long time:
+
+  -- wait_for_unblock_async
+
+  -- run_tac
+  --   while true do
+  --     if (← Server.Test.Cancel.unblockedCancelTk.isSet) then
+  --       break
+  --     IO.sleep 30
+
+  -- sleep 100000
+  exact testSorry
+
+theorem bar : 2 * a = 2 * b := by
+  congr 1
+  -- apply a_eq_b
+  simp only [a_eq_b]
+  run_tac
+    Server.Test.Cancel.unblockedCancelTk.set

tests/lean/isDefEqOffsetBug.lean

@@ -16,4 +16,4 @@ theorem subZero [AddGroup α] {a : α} : a + -(0 : α) = a := by
   rw [addZero]
 
 theorem shouldFail [AddGroup α] : ((0 : α) + 0) = 0 :=
-  rfl -- Error
+  (rfl) -- Error

tests/lean/isDefEqOffsetBug.lean.expected.out

@@ -1,4 +1,4 @@
-isDefEqOffsetBug.lean:19:2-19:5: error: type mismatch
+isDefEqOffsetBug.lean:19:2-19:7: error: type mismatch
   rfl
 has type
   ?m = ?m : Prop

tests/lean/run/2961.lean

@@ -8,12 +8,12 @@ def replace (f : Nat → Option Nat) (t : Nat) : Nat :=
 
 /--
 info: equations:
-theorem replace.eq_1 : ∀ (f : Nat → Option Nat),
+@[defeq] theorem replace.eq_1 : ∀ (f : Nat → Option Nat),
   replace f Nat.zero =
     match f Nat.zero with
     | some u => u
     | none => Nat.zero
-theorem replace.eq_2 : ∀ (f : Nat → Option Nat) (t' : Nat),
+@[defeq] theorem replace.eq_2 : ∀ (f : Nat → Option Nat) (t' : Nat),
   replace f t'.succ =
     match f t'.succ with
     | some u => u
@@ -58,12 +58,12 @@ def replace2 (f : Nat → Option Nat) (t1 t2 : Nat) : Nat :=
 
 /--
 info: equations:
-theorem replace2.eq_1 : ∀ (f : Nat → Option Nat) (t1 : Nat),
+@[defeq] theorem replace2.eq_1 : ∀ (f : Nat → Option Nat) (t1 : Nat),
   replace2 f t1 Nat.zero =
     match f t1 with
     | some u => u
     | none => Nat.zero
-theorem replace2.eq_2 : ∀ (f : Nat → Option Nat) (t1 t' : Nat),
+@[defeq] theorem replace2.eq_2 : ∀ (f : Nat → Option Nat) (t1 t' : Nat),
   replace2 f t1 t'.succ =
     match f t1 with
     | some u => u

tests/lean/run/5667.lean

@@ -92,8 +92,8 @@ def optimize2 : Expr → Expr
 
 /--
 info: equations:
-theorem optimize2.eq_1 : ∀ (i : BitVec 32), optimize2 (Expr.const i) = Expr.const i
-theorem optimize2.eq_2 : ∀ (bop : Unit) (e1 : Expr),
+@[defeq] theorem optimize2.eq_1 : ∀ (i : BitVec 32), optimize2 (Expr.const i) = Expr.const i
+@[defeq] theorem optimize2.eq_2 : ∀ (bop : Unit) (e1 : Expr),
   optimize2 (Expr.op bop e1) =
     match optimize2 e1 with
     | Expr.const i => Expr.op bop (Expr.const 0)
@@ -113,8 +113,8 @@ def optimize3 : Expr → Expr
 
 /--
 info: equations:
-theorem optimize3.eq_1 : ∀ (i : BitVec 32), optimize3 (Expr.const i) = Expr.const i
-theorem optimize3.eq_2 : ∀ (bop : Unit) (i : BitVec 32),
+@[defeq] theorem optimize3.eq_1 : ∀ (i : BitVec 32), optimize3 (Expr.const i) = Expr.const i
+@[defeq] theorem optimize3.eq_2 : ∀ (bop : Unit) (i : BitVec 32),
   optimize3 (Expr.op bop (Expr.const i)) = Expr.op bop (optimize3 (Expr.const i))
 theorem optimize3.eq_3 : ∀ (bop : Unit) (e1 : Expr),
   (∀ (i : BitVec 32), e1 = Expr.const i → False) → optimize3 (Expr.op bop e1) = Expr.const 0

tests/lean/run/6789.lean

@@ -36,7 +36,7 @@ theorem Extension.recOn'.eq_1.{v} : ∀ {motive : (Γ Δ : Con) → Extension Γ
   (zero : {Γ : Con} → motive Γ Γ Extension.zero)
   (succ : {Γ Δ : Con} → (xt : Extension Γ Δ) → (A : Nat) → motive Γ Δ xt → motive Γ (Δ.ext A) (xt.succ A)) (x : Con),
   Extension.recOn' zero succ Extension.zero = zero
-theorem Extension.recOn'.eq_2.{v} : ∀ {motive : (Γ Δ : Con) → Extension Γ Δ → Sort v}
+@[defeq] theorem Extension.recOn'.eq_2.{v} : ∀ {motive : (Γ Δ : Con) → Extension Γ Δ → Sort v}
   (zero : {Γ : Con} → motive Γ Γ Extension.zero)
   (succ : {Γ Δ : Con} → (xt : Extension Γ Δ) → (A : Nat) → motive Γ Δ xt → motive Γ (Δ.ext A) (xt.succ A)) (x Δ : Con)
   (A : Nat) (xt : Extension x Δ),
@@ -53,9 +53,9 @@ def Extension.pullback_con
 
 /--
 info: equations:
-theorem Extension.pullback_con.eq_1.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B),
+@[defeq] theorem Extension.pullback_con.eq_1.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B),
   Extension.zero.pullback_con x = B'
-theorem Extension.pullback_con.eq_2.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B) (Δ_2 : Con)
+@[defeq] theorem Extension.pullback_con.eq_2.{u} : ∀ {Op : Con → Con → Type u} {B B' : Con} (x : Op B' B) (Δ_2 : Con)
   (xt : Extension B Δ_2) (A : Nat), (xt.succ A).pullback_con x = (xt.pullback_con x).ext A
 -/
 #guard_msgs in

tests/lean/run/def20.lean

@@ -6,8 +6,7 @@ def f : Char → Nat
 | 'e' => 4
 | _   => 5
 
-theorem ex1 : (f 'a', f 'b', f 'c', f 'd', f 'e', f 'f') = (0, 1, 2, 3, 4, 5) :=
-rfl
+theorem ex1 : (f 'a', f 'b', f 'c', f 'd', f 'e', f 'f') = (0, 1, 2, 3, 4, 5) := rfl
 
 def g : Nat → Nat
 | 100000 => 0
@@ -16,8 +15,10 @@ def g : Nat → Nat
 | 400000 => 3
 | _      => 5
 
-theorem ex2 : (g 100000, g 200000, g 300000, g 400000, g 0) = (0, 1, 2, 3, 5) :=
-rfl
+-- This uses `(rfl)` and no `rfl` to avoid the `rfl` attribute kicking in
+-- and trying to prove the theorem with full transparency and without smart unfolding,
+-- which goes wrong
+theorem ex2 : (g 100000, g 200000, g 300000, g 400000, g 0) = (0, 1, 2, 3, 5) := (rfl)
 
 def h : String → Nat
 | "hello" => 0

tests/lean/run/defeqAttrib.lean

@@ -0,0 +1,93 @@
+axiom testSorry : α
+
+opaque a : Nat
+opaque b : Nat
+def c := a
+@[irreducible] def d := a
+opaque P : Nat → Prop
+
+@[irreducible] def ac := a = c
+
+/--
+error: Not a definitional equality: the left-hand side
+  a
+is not definitionally equal to the right-hand side
+  b
+-/
+#guard_msgs in
+@[defeq] theorem a_eq_b : a = b := testSorry
+theorem a_eq_c : a = c := rfl
+@[defeq] theorem a_eq_c' : a = c := Eq.refl _
+theorem a_eq_c'' : a = c := Eq.refl _
+@[defeq] theorem a_eq_c''' : ac := by with_unfolding_all rfl
+@[defeq] theorem a_eq_d : a = d := by simp [d]
+
+/-- error: Not a definitional equality: the conclusion should be an equality, but is True -/
+#guard_msgs in
+@[defeq] def not_an_eq : True := trivial
+
+
+def Tricky.rfl := a_eq_b
+/--
+error: Not a definitional equality: the left-hand side
+  a
+is not definitionally equal to the right-hand side
+  b
+-/
+#guard_msgs in
+theorem Tricky.a_eq_b : a = b := rfl -- to confuse the heuristics
+
+/-! Does `#print` show the attribute? -/
+
+/-- info: @[defeq] theorem a_eq_c : a = c -/
+#guard_msgs in
+#print sig a_eq_c
+
+/-! Does dsimp use it? -/
+
+/-- error: dsimp made no progress -/
+#guard_msgs in example (h : P b) : P a := by dsimp [a_eq_b]; exact h
+
+/-- error: dsimp made no progress -/
+#guard_msgs in example (h : P b) : P a := by dsimp [Tricky.a_eq_b]; exact h
+
+#guard_msgs in example (h : P c) : P a := by dsimp [a_eq_c]; exact h
+
+#guard_msgs in example (h : P c) : P a := by dsimp [a_eq_c']; exact h
+
+/-- error: dsimp made no progress -/
+#guard_msgs in example (h : P c) : P a := by dsimp [a_eq_c'']; exact h
+
+-- a_eq_c''' is correctly tagged, but not used by `a_eq_c` because simp does not look through `ac`.
+/-- error: dsimp made no progress -/
+#guard_msgs in example (h : P c) : P a := by dsimp [a_eq_c''']; exact h
+
+#guard_msgs in example (h : P d) : P a := by dsimp [a_eq_d]; exact h
+
+-- Order of simp and rfl attribute
+def e1 := a
+@[simp] theorem e1_eq_a : e1 = a := rfl
+#guard_msgs in example (h : P a) : P e1 := by dsimp; exact h
+
+def e2 := a
+@[defeq,simp] theorem e2_eq_a : e2 = a := (rfl)
+#guard_msgs in example (h : P a) : P e2 := by dsimp; exact h
+
+def e3 := a
+@[simp,defeq] theorem e3_eq_a : e2 = a := (rfl) -- defeq has to come before simp
+/-- error: dsimp made no progress -/
+#guard_msgs in example (h : P a) : P e3 := by dsimp; exact h
+
+-- Tests the `defeq` attibute on a realized constant: That they are set, and that they
+-- are transported out
+def f := a
+#guard_msgs in example (h : P a) : P f := by dsimp [f]; exact h
+#guard_msgs in example (h : P a) : P f := by dsimp [f.eq_1]; exact h
+#guard_msgs in example (h : P a) : P f := by dsimp [f.eq_def]; exact h
+#guard_msgs in example (h : P a) : P f := by dsimp [f.eq_unfold]; exact h
+
+
+def Q := 1 = 1
+@[defeq, simp] theorem Q_true : Q := rfl
+/-- error: dsimp made no progress -/
+#guard_msgs in example : Q := by dsimp [Q_true]

tests/lean/run/dsimp1.lean

@@ -22,8 +22,14 @@ example (x : Nat) : P (id x.succ.succ).isZero := by
   dsimp [Nat.isZero]
   apply P_false
 
+/--
+trace: x : Nat
+⊢ P false
+-/
+#guard_msgs in
 example (x : Nat) : P (id x.succ.succ).isZero := by
   dsimp [Nat.isZero.eq_2]
+  trace_state
   apply P_false
 
 example (x : Nat) : P (id x.succ.succ).isZero := by

tests/lean/run/eqnOptions.lean

@@ -7,8 +7,8 @@ def nonrecfun : Bool → Nat
 
 /--
 info: equations:
-theorem Test1.nonrecfun.eq_1 : nonrecfun false = 0
-theorem Test1.nonrecfun.eq_2 : nonrecfun true = 0
+@[defeq] theorem Test1.nonrecfun.eq_1 : nonrecfun false = 0
+@[defeq] theorem Test1.nonrecfun.eq_2 : nonrecfun true = 0
 -/
 #guard_msgs in
 #print equations nonrecfun
@@ -24,7 +24,7 @@ def nonrecfun : Bool → Nat
 
 /--
 info: equations:
-theorem Test2.nonrecfun.eq_1 : ∀ (x : Bool),
+@[defeq] theorem Test2.nonrecfun.eq_1 : ∀ (x : Bool),
   nonrecfun x =
     match x with
     | false => 0
@@ -46,8 +46,8 @@ set_option backward.eqns.nonrecursive false
 
 /--
 info: equations:
-theorem Test3.nonrecfun.eq_1 : nonrecfun false = 0
-theorem Test3.nonrecfun.eq_2 : nonrecfun true = 0
+@[defeq] theorem Test3.nonrecfun.eq_1 : nonrecfun false = 0
+@[defeq] theorem Test3.nonrecfun.eq_2 : nonrecfun true = 0
 -/
 #guard_msgs in
 #print equations nonrecfun

tests/lean/run/issue5661.lean

@@ -8,7 +8,7 @@ inductive Nested where
   | other
 
 /--
-info: theorem Nested.nest.sizeOf_spec : ∀ (a : StructLike Nested), sizeOf (Nested.nest a) = 1 + sizeOf a :=
+info: @[defeq] theorem Nested.nest.sizeOf_spec : ∀ (a : StructLike Nested), sizeOf (Nested.nest a) = 1 + sizeOf a :=
 fun a => Eq.refl (1 + sizeOf a)
 -/
 #guard_msgs in

tests/lean/run/partial_fixpoint.lean

@@ -13,7 +13,7 @@ partial_fixpoint
 
 /--
 info: equations:
-theorem loop.eq_1 : ∀ (x : Nat), loop x = loop (x + 1)
+@[defeq] theorem loop.eq_1 : ∀ (x : Nat), loop x = loop (x + 1)
 -/
 #guard_msgs in
 #print equations loop

tests/lean/run/printEqns.lean

@@ -1,3 +1,8 @@
+/-!
+
+Re-instantiate these after a stage0 update
+
+
 /--
 info: equations:
 theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), [].append x = x
@@ -14,6 +19,8 @@ theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : Lis
 #guard_msgs in
 #print equations List.append
 
+-/
+
 @[simp] def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1

tests/lean/run/proofAsSorry.lean

@@ -14,7 +14,7 @@ example : 2 + 2 = 5 := rfl -- This is not a theorem
 
 /-- warning: declaration uses 'sorry' -/
 #guard_msgs in
-theorem ex : 2 + 2 = 5 := rfl
+theorem ex : 2 + 2 = 5 := id rfl -- id rfl to avoid the rfl attribute kicking in
 
 #guard_msgs in
 def data (w : Nat) : String := toString w

tests/lean/run/structuralOverNested.lean

@@ -31,7 +31,7 @@ def RTree.simple_size : RTree α → Nat
   | .node _x t _ts => 1 + (t true).simple_size + (t false).simple_size
 
 /--
-info: theorem RTree.simple_size.eq_1.{u_1} : ∀ {α : Type u_1} (_x : α) (t : Bool → RTree α) (_ts : List (RTree α)),
+info: @[defeq] theorem RTree.simple_size.eq_1.{u_1} : ∀ {α : Type u_1} (_x : α) (t : Bool → RTree α) (_ts : List (RTree α)),
   (RTree.node _x t _ts).simple_size = 1 + (t true).simple_size + (t false).simple_size :=
 fun {α} _x t _ts => Eq.refl (RTree.node _x t _ts).simple_size
 -/
@@ -51,7 +51,7 @@ def RTree.aux_size : List (RTree α) → Nat
 end
 
 /--
-info: theorem RTree.aux_size.eq_2.{u_1} : ∀ {α : Type u_1} (t : RTree α) (ts : List (RTree α)),
+info: @[defeq] theorem RTree.aux_size.eq_2.{u_1} : ∀ {α : Type u_1} (t : RTree α) (ts : List (RTree α)),
   RTree.aux_size (t :: ts) = t.size + RTree.aux_size ts :=
 fun {α} t ts => Eq.refl (RTree.aux_size (t :: ts))
 -/
@@ -67,8 +67,8 @@ def RTree.map_aux (f : α → β) : List (RTree α) → List (RTree β)
 end
 
 /--
-info: theorem RTree.map_aux.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : RTree α) (ts : List (RTree α)),
-  RTree.map_aux f (t :: ts) = RTree.map f t :: RTree.map_aux f ts :=
+info: @[defeq] theorem RTree.map_aux.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (t : RTree α)
+  (ts : List (RTree α)), RTree.map_aux f (t :: ts) = RTree.map f t :: RTree.map_aux f ts :=
 fun {α} {β} f t ts => Eq.refl (RTree.map_aux f (t :: ts))
 -/
 #guard_msgs in
@@ -95,7 +95,7 @@ def VTree.vec_size : Vec (VTree α true 5) n b → Nat
 end
 
 /--
-info: theorem VTree.size.eq_1.{u_1} : ∀ {α : Type u_1} (b_2 : Bool) (n_2 : Nat) (a : α)
+info: @[defeq] theorem VTree.size.eq_1.{u_1} : ∀ {α : Type u_1} (b_2 : Bool) (n_2 : Nat) (a : α)
   (f : List Bool → List Nat → Vec (VTree α true 5) n_2 b_2),
   (VTree.node b_2 n_2 a f).size = 1 + VTree.vec_size (f [] []) :=
 fun {α} b_2 n_2 a f => Eq.refl (VTree.node b_2 n_2 a f).size

tests/lean/run/unfoldLemma.lean

@@ -4,8 +4,8 @@ def Option_map (f : α → β) : Option α → Option β
 
 /--
 info: equations:
-theorem Option_map.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Option_map f none = none
-theorem Option_map.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x_1 : α),
+@[defeq] theorem Option_map.eq_1.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Option_map f none = none
+@[defeq] theorem Option_map.eq_2.{u_1, u_2} : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x_1 : α),
   Option_map f (some x_1) = some (f x_1)
 -/
 #guard_msgs in

tests/lean/run/wfEqns5.lean

@@ -87,9 +87,9 @@ termination_by structural n => n
 
 /--
 info: equations:
-theorem Structural.foo.eq_1 : foo 0 0 = 0
+@[defeq] theorem Structural.foo.eq_1 : foo 0 0 = 0
 theorem Structural.foo.eq_2 : ∀ (x : Nat), (x = 0 → False) → foo 0 x = x
-theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
+@[defeq] theorem Structural.foo.eq_3 : ∀ (x n : Nat), foo n.succ x = foo n x
 -/
 #guard_msgs in
 #print equations foo

tests/pkg/module/Module/Basic.lean

@@ -1,17 +1,100 @@
 module
 
+axiom testSorry : α
+
 /-! Module docstring -/
 
-/-- A definition. -/
+/-- A definition (not exposed). -/
 def f := 1
+/-- An definition (exposed) -/
+@[expose] def fexp := 1
 
 #guard_msgs(drop warning) in
 /-- A theorem. -/
-theorem t : f = 1 := sorry
+theorem t : f = 1 := testSorry
 
+-- Check that the theorem types are checked in exported context, where `f` is not defeq to `1`
+-- (but `fexp` is)
+
+/--
+error: type mismatch
+  y
+has type
+  Vector Unit 1 : Type
+but is expected to have type
+  Vector Unit f : Type
+-/
+#guard_msgs in
+theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry
+
+private theorem v' (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry
+
+private theorem v'' (x : Vector Unit fexp) (y : Vector Unit 1) : x = y := testSorry
+
+-- Check that rfl theorems are complained about if they aren't rfl in the context of their type
+
+/--
+error: Not a definitional equality: the left-hand side
+  f
+is not definitionally equal to the right-hand side
+  1
+
+Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed.
+-/
+#guard_msgs in
 theorem trfl : f = 1 := rfl
+/--
+error: Not a definitional equality: the left-hand side
+  f
+is not definitionally equal to the right-hand side
+  1
 
-@[expose] def fexp := 1
+Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed.
+-/
+#guard_msgs in
+@[defeq] theorem trfl' : f = 1 := (rfl)
+
+private theorem trflprivate : f = 1 := rfl
+private def trflprivate' : f = 1 := rfl
+@[defeq] private def trflprivate''' : f = 1 := rfl
+private theorem trflprivate'''' : f = 1 := (rfl)
+
+theorem fexp_trfl : fexp = 1 := rfl
+@[defeq] theorem fexp_trfl' : fexp = 1 := rfl
+
+opaque P : Nat → Prop
+axiom hP1 : P 1
+
+/-- error: dsimp made no progress -/
+#guard_msgs in
+example : P f := by dsimp only [t]; exact hP1
+example : P f := by simp only [t]; exact hP1
+
+/-- error: dsimp made no progress -/
+#guard_msgs in
+example : P f := by dsimp only [trfl]; exact hP1
+/-- error: dsimp made no progress -/
+#guard_msgs in
+example : P f := by dsimp only [trfl']; exact hP1
+example : P f := by dsimp only [trflprivate]; exact hP1
+example : P f := by dsimp only [trflprivate']; exact hP1
+
+
+example : P fexp := by dsimp only [fexp_trfl]; exact hP1
+example : P fexp := by dsimp only [fexp_trfl]; exact hP1
+
+
+-- Check that the error message does not mention the export issue if
+-- it wouldn’t be a rfl otherwise either
+
+/--
+error: Not a definitional equality: the left-hand side
+  f
+is not definitionally equal to the right-hand side
+  2
+-/
+#guard_msgs in
+@[defeq] theorem not_rfl : f = 2 := testSorry
 
 private def priv := 2
 
@@ -52,90 +135,74 @@ def f.eq_def := 1
 #guard_msgs in
 def fexp.eq_def := 1
 
-/-- info: f.eq_def : f = 1 -/
-#guard_msgs in
-#check f.eq_def
+/-- info: @[defeq] private theorem f.eq_def : f = 1 -/
+#guard_msgs in #print sig f.eq_def
 
-/-- info: f.eq_unfold : f = 1 -/
-#guard_msgs in
-#check f.eq_unfold
+/-- info: @[defeq] private theorem f.eq_unfold : f = 1 -/
+#guard_msgs in #print sig f.eq_unfold
 
-/-- info: fexp.eq_def : fexp = 1 -/
-#guard_msgs in
-#check fexp.eq_def
+/-- info: @[defeq] theorem fexp.eq_def : fexp = 1 -/
+#guard_msgs in #print sig fexp.eq_def
 
-/-- info: fexp.eq_unfold : fexp = 1 -/
-#guard_msgs in
-#check fexp.eq_unfold
+/-- info: @[defeq] theorem fexp.eq_unfold : fexp = 1 -/
+#guard_msgs in #print sig fexp.eq_unfold
 
-/-- info: f_struct.eq_1 : f_struct 0 = 0 -/
-#guard_msgs in
-#check f_struct.eq_1
+/-- info: @[defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/
+#guard_msgs in #print sig f_struct.eq_1
 
 /--
-info: f_struct.eq_def (x✝ : Nat) :
-  f_struct x✝ =
-    match x✝ with
-    | 0 => 0
-    | n.succ => f_struct n
--/
-#guard_msgs in
-#check f_struct.eq_def
-
-/--
-info: f_struct.eq_unfold :
-  f_struct = fun x =>
+info: private theorem f_struct.eq_def : ∀ (x : Nat),
+  f_struct x =
     match x with
     | 0 => 0
     | n.succ => f_struct n
 -/
-#guard_msgs(pass trace, all) in
-#check f_struct.eq_unfold
-
-/-- info: f_wfrec.eq_1 (x✝ : Nat) : f_wfrec 0 x✝ = x✝ -/
-#guard_msgs(pass trace, all) in
-#check f_wfrec.eq_1
+#guard_msgs in #print sig f_struct.eq_def
 
 /--
-info: f_wfrec.eq_def (x✝ x✝¹ : Nat) :
-  f_wfrec x✝ x✝¹ =
-    match x✝, x✝¹ with
-    | 0, acc => acc
-    | n.succ, acc => f_wfrec n (acc + 1)
+info: private theorem f_struct.eq_unfold : f_struct = fun x =>
+  match x with
+  | 0 => 0
+  | n.succ => f_struct n
 -/
-#guard_msgs in
-#check f_wfrec.eq_def
+#guard_msgs(pass trace, all) in #print sig f_struct.eq_unfold
+
+/-- info: private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
+#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1
 
 /--
-info: f_wfrec.eq_unfold :
-  f_wfrec = fun x x_1 =>
+info: private theorem f_wfrec.eq_def : ∀ (x x_1 : Nat),
+  f_wfrec x x_1 =
     match x, x_1 with
     | 0, acc => acc
     | n.succ, acc => f_wfrec n (acc + 1)
 -/
-#guard_msgs in
-#check f_wfrec.eq_unfold
-
-/-- info: f_exp_wfrec.eq_1 (x✝ : Nat) : f_exp_wfrec 0 x✝ = x✝ -/
-#guard_msgs in
-#check f_exp_wfrec.eq_1
+#guard_msgs in #print sig f_wfrec.eq_def
 
 /--
-info: f_exp_wfrec.eq_def (x✝ x✝¹ : Nat) :
-  f_exp_wfrec x✝ x✝¹ =
-    match x✝, x✝¹ with
-    | 0, acc => acc
-    | n.succ, acc => f_exp_wfrec n (acc + 1)
+info: private theorem f_wfrec.eq_unfold : f_wfrec = fun x x_1 =>
+  match x, x_1 with
+  | 0, acc => acc
+  | n.succ, acc => f_wfrec n (acc + 1)
 -/
-#guard_msgs in
-#check f_exp_wfrec.eq_def
+#guard_msgs in #print sig f_wfrec.eq_unfold
+
+/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
+#guard_msgs in #print sig f_exp_wfrec.eq_1
 
 /--
-info: f_exp_wfrec.eq_unfold :
-  f_exp_wfrec = fun x x_1 =>
+info: theorem f_exp_wfrec.eq_def : ∀ (x x_1 : Nat),
+  f_exp_wfrec x x_1 =
     match x, x_1 with
     | 0, acc => acc
     | n.succ, acc => f_exp_wfrec n (acc + 1)
 -/
-#guard_msgs in
-#check f_exp_wfrec.eq_unfold
+#guard_msgs in #print sig f_exp_wfrec.eq_def
+
+/--
+info: theorem f_exp_wfrec.eq_unfold : f_exp_wfrec = fun x x_1 =>
+  match x, x_1 with
+  | 0, acc => acc
+  | n.succ, acc => f_exp_wfrec n (acc + 1)
+-/
+#guard_msgs in #print sig f_exp_wfrec.eq_unfold

tests/pkg/module/Module/Imported.lean

@@ -3,6 +3,15 @@ module
 prelude
 import Module.Basic
 
+/-! Definitions should be exported without their bodies by default -/
+
+/--
+info: def f : Nat :=
+<not imported>
+-/
+#guard_msgs in
+#print f
+
 /-! Theorems should be exported without their bodies -/
 
 /--
@@ -12,10 +21,27 @@ info: theorem t : f = 1 :=
 #guard_msgs in
 #print t
 
+/--
+info: theorem trfl : f = 1 :=
+<not imported>
+-/
+#guard_msgs in
+#print trfl
+
 /-- error: dsimp made no progress -/
 #guard_msgs in
-example : f = 1 := by dsimp only [t]
+example : P f := by dsimp only [t]; exact hP1
+example : P f := by simp only [t]; exact hP1
 
+/-- error: dsimp made no progress -/
+#guard_msgs in
+example : P f := by dsimp only [trfl]; exact hP1
+/-- error: dsimp made no progress -/
+#guard_msgs in
+example : P f := by dsimp only [trfl']; exact hP1
+
+example : P fexp := by dsimp only [fexp_trfl]; exact hP1
+example : P fexp := by dsimp only [fexp_trfl']; exact hP1
 example : t = t := by dsimp only [trfl]
 
 /--

tests/pkg/module/Module/ImportedAll.lean

@@ -7,7 +7,7 @@ import all Module.Basic
 
 /--
 info: theorem t : f = 1 :=
-sorry
+testSorry
 -/
 #guard_msgs in
 #print t
@@ -23,100 +23,116 @@ but is expected to have type
 #guard_msgs in
 theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := sorry
 
-
-
-/-- info: f.eq_def : f = 1 -/
+/-- error: dsimp made no progress -/
 #guard_msgs in
-#check f.eq_def
+example : P f := by dsimp only [t]; exact hP1
+example : P f := by simp only [t]; exact hP1
 
-/-- info: f.eq_unfold : f = 1 -/
+/-- error: dsimp made no progress -/
 #guard_msgs in
-#check f.eq_unfold
-
-/-- info: f_struct.eq_1 : f_struct 0 = 0 -/
+example : P f := by dsimp only [trfl]; exact hP1
+/-- error: dsimp made no progress -/
 #guard_msgs in
-#check f_struct.eq_1
+example : P f := by dsimp only [trfl']; exact hP1
 
 /--
-info: f_struct.eq_def (x✝ : Nat) :
-  f_struct x✝ =
-    match x✝ with
-    | 0 => 0
-    | n.succ => f_struct n
+error: unknown identifier 'trflprivate'
+---
+error: dsimp made no progress
 -/
 #guard_msgs in
-#check f_struct.eq_def
+example : P f := by dsimp only [trflprivate]; exact hP1
+/--
+error: unknown identifier 'trflprivate''
+---
+error: dsimp made no progress
+-/
+#guard_msgs in
+example : P f := by dsimp only [trflprivate']; exact hP1
+
+
+example : P fexp := by dsimp only [fexp_trfl]; exact hP1
+example : P fexp := by dsimp only [fexp_trfl']; exact hP1
+
+
+/-- info: @[defeq] private theorem f.eq_def : f = 1 -/
+#guard_msgs in #print sig f.eq_def
+
+/-- info: @[defeq] private theorem f.eq_unfold : f = 1 -/
+#guard_msgs in #print sig f.eq_unfold
+
+/-- info: @[defeq] private theorem f_struct.eq_1 : f_struct 0 = 0 -/
+#guard_msgs in #print sig f_struct.eq_1
 
 /--
-info: f_struct.eq_unfold :
-  f_struct = fun x =>
+info: private theorem f_struct.eq_def : ∀ (x : Nat),
+  f_struct x =
     match x with
     | 0 => 0
     | n.succ => f_struct n
 -/
-#guard_msgs in
-#check f_struct.eq_unfold
-
-/-- info: f_wfrec.eq_1 (x✝ : Nat) : f_wfrec 0 x✝ = x✝ -/
-#guard_msgs(pass trace, all) in
-#check f_wfrec.eq_1
+#guard_msgs in #print sig f_struct.eq_def
 
 /--
-info: f_wfrec.eq_def (x✝ x✝¹ : Nat) :
-  f_wfrec x✝ x✝¹ =
-    match x✝, x✝¹ with
-    | 0, acc => acc
-    | n.succ, acc => f_wfrec n (acc + 1)
+info: private theorem f_struct.eq_unfold : f_struct = fun x =>
+  match x with
+  | 0 => 0
+  | n.succ => f_struct n
 -/
-#guard_msgs(pass trace, all) in
-#check f_wfrec.eq_def
+#guard_msgs in #print sig f_struct.eq_unfold
+
+/-- info: private theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
+#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1
 
 /--
-info: f_wfrec.eq_unfold :
-  f_wfrec = fun x x_1 =>
+info: private theorem f_wfrec.eq_def : ∀ (x x_1 : Nat),
+  f_wfrec x x_1 =
     match x, x_1 with
     | 0, acc => acc
     | n.succ, acc => f_wfrec n (acc + 1)
 -/
-#guard_msgs(pass trace, all) in
-#check f_wfrec.eq_unfold
+#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_def
 
 /--
-info: f_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc acc)
-  (case2 : ∀ (n acc : Nat), motive n (acc + 1) (f_wfrec n (acc + 1)) → motive n.succ acc (f_wfrec n (acc + 1)))
-  (a✝ a✝¹ : Nat) : motive a✝ a✝¹ (f_wfrec a✝ a✝¹)
+info: private theorem f_wfrec.eq_unfold : f_wfrec = fun x x_1 =>
+  match x, x_1 with
+  | 0, acc => acc
+  | n.succ, acc => f_wfrec n (acc + 1)
 -/
-#guard_msgs(pass trace, all) in
-#check f_wfrec.induct_unfolding
-
-/-- info: f_exp_wfrec.eq_1 (x✝ : Nat) : f_exp_wfrec 0 x✝ = x✝ -/
-#guard_msgs in
-#check f_exp_wfrec.eq_1
+#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_unfold
 
 /--
-info: f_exp_wfrec.eq_def (x✝ x✝¹ : Nat) :
-  f_exp_wfrec x✝ x✝¹ =
-    match x✝, x✝¹ with
-    | 0, acc => acc
-    | n.succ, acc => f_exp_wfrec n (acc + 1)
+info: theorem f_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → Prop),
+  (∀ (acc : Nat), motive 0 acc acc) →
+    (∀ (n acc : Nat), motive n (acc + 1) (f_wfrec n (acc + 1)) → motive n.succ acc (f_wfrec n (acc + 1))) →
+      ∀ (a a_1 : Nat), motive a a_1 (f_wfrec a a_1)
 -/
-#guard_msgs in
-#check f_exp_wfrec.eq_def
+#guard_msgs(pass trace, all) in #print sig f_wfrec.induct_unfolding
+
+/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
+#guard_msgs in #print sig f_exp_wfrec.eq_1
 
 /--
-info: f_exp_wfrec.eq_unfold :
-  f_exp_wfrec = fun x x_1 =>
+info: theorem f_exp_wfrec.eq_def : ∀ (x x_1 : Nat),
+  f_exp_wfrec x x_1 =
     match x, x_1 with
     | 0, acc => acc
     | n.succ, acc => f_exp_wfrec n (acc + 1)
 -/
-#guard_msgs in
-#check f_exp_wfrec.eq_unfold
+#guard_msgs in #print sig f_exp_wfrec.eq_def
 
 /--
-info: f_exp_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc acc)
-  (case2 : ∀ (n acc : Nat), motive n (acc + 1) (f_exp_wfrec n (acc + 1)) → motive n.succ acc (f_exp_wfrec n (acc + 1)))
-  (a✝ a✝¹ : Nat) : motive a✝ a✝¹ (f_exp_wfrec a✝ a✝¹)
+info: theorem f_exp_wfrec.eq_unfold : f_exp_wfrec = fun x x_1 =>
+  match x, x_1 with
+  | 0, acc => acc
+  | n.succ, acc => f_exp_wfrec n (acc + 1)
 -/
-#guard_msgs(pass trace, all) in
-#check f_exp_wfrec.induct_unfolding
+#guard_msgs in #print sig f_exp_wfrec.eq_unfold
+
+/--
+info: theorem f_exp_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → Prop),
+  (∀ (acc : Nat), motive 0 acc acc) →
+    (∀ (n acc : Nat), motive n (acc + 1) (f_exp_wfrec n (acc + 1)) → motive n.succ acc (f_exp_wfrec n (acc + 1))) →
+      ∀ (a a_1 : Nat), motive a a_1 (f_exp_wfrec a a_1)
+-/
+#guard_msgs(pass trace, all) in #print sig f_exp_wfrec.induct_unfolding

tests/pkg/module/Module/NonModule.lean

@@ -1,98 +1,84 @@
 import Module.Basic
 import Lean
 
-/-- info: f.eq_def : f = 1 -/
-#guard_msgs in
-#check f.eq_def
+/-- info: @[defeq] theorem f.eq_def : f = 1 -/
+#guard_msgs in #print sig f.eq_def
 
-/-- info: f.eq_unfold : f = 1 -/
-#guard_msgs in
-#check f.eq_unfold
-
-/-- info: f_struct.eq_1 : f_struct 0 = 0 -/
-#guard_msgs in
-#check f_struct.eq_1
+/-- info: @[defeq] theorem f.eq_unfold : f = 1 -/
+#guard_msgs in #print sig f.eq_unfold
 
+/-- info: @[defeq] theorem f_struct.eq_1 : f_struct 0 = 0 -/
+#guard_msgs in #print sig f_struct.eq_1
 /--
-info: f_struct.eq_def (x✝ : Nat) :
-  f_struct x✝ =
-    match x✝ with
-    | 0 => 0
-    | n.succ => f_struct n
--/
-#guard_msgs in
-#check f_struct.eq_def
-
-/--
-info: f_struct.eq_unfold :
-  f_struct = fun x =>
+info: theorem f_struct.eq_def : ∀ (x : Nat),
+  f_struct x =
     match x with
     | 0 => 0
     | n.succ => f_struct n
 -/
-#guard_msgs in
-#check f_struct.eq_unfold
-
-/-- info: f_wfrec.eq_1 (x✝ : Nat) : f_wfrec 0 x✝ = x✝ -/
-#guard_msgs(pass trace, all) in
-#check f_wfrec.eq_1
+#guard_msgs in #print sig f_struct.eq_def
 
 /--
-info: f_wfrec.eq_def (x✝ x✝¹ : Nat) :
-  f_wfrec x✝ x✝¹ =
-    match x✝, x✝¹ with
-    | 0, acc => acc
-    | n.succ, acc => f_wfrec n (acc + 1)
+info: theorem f_struct.eq_unfold : f_struct = fun x =>
+  match x with
+  | 0 => 0
+  | n.succ => f_struct n
 -/
-#guard_msgs(pass trace, all) in
-#check f_wfrec.eq_def
+#guard_msgs in #print sig f_struct.eq_unfold
+
+/-- info: theorem f_wfrec.eq_1 : ∀ (x : Nat), f_wfrec 0 x = x -/
+#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_1
 
 /--
-info: f_wfrec.eq_unfold :
-  f_wfrec = fun x x_1 =>
+info: theorem f_wfrec.eq_def : ∀ (x x_1 : Nat),
+  f_wfrec x x_1 =
     match x, x_1 with
     | 0, acc => acc
     | n.succ, acc => f_wfrec n (acc + 1)
 -/
-#guard_msgs(pass trace, all) in
-#check f_wfrec.eq_unfold
+#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_def
 
 /--
-info: f_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc acc)
-  (case2 : ∀ (n acc : Nat), motive n (acc + 1) (f_wfrec n (acc + 1)) → motive n.succ acc (f_wfrec n (acc + 1)))
-  (a✝ a✝¹ : Nat) : motive a✝ a✝¹ (f_wfrec a✝ a✝¹)
+info: theorem f_wfrec.eq_unfold : f_wfrec = fun x x_1 =>
+  match x, x_1 with
+  | 0, acc => acc
+  | n.succ, acc => f_wfrec n (acc + 1)
 -/
-#guard_msgs(pass trace, all) in
-#check f_wfrec.induct_unfolding
-
-/-- info: f_exp_wfrec.eq_1 (x✝ : Nat) : f_exp_wfrec 0 x✝ = x✝ -/
-#guard_msgs(pass trace, all) in
-#check f_exp_wfrec.eq_1
+#guard_msgs(pass trace, all) in #print sig f_wfrec.eq_unfold
 
 /--
-info: f_exp_wfrec.eq_def (x✝ x✝¹ : Nat) :
-  f_exp_wfrec x✝ x✝¹ =
-    match x✝, x✝¹ with
-    | 0, acc => acc
-    | n.succ, acc => f_exp_wfrec n (acc + 1)
+info: theorem f_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → Prop),
+  (∀ (acc : Nat), motive 0 acc acc) →
+    (∀ (n acc : Nat), motive n (acc + 1) (f_wfrec n (acc + 1)) → motive n.succ acc (f_wfrec n (acc + 1))) →
+      ∀ (a a_1 : Nat), motive a a_1 (f_wfrec a a_1)
 -/
-#guard_msgs in
-#check f_exp_wfrec.eq_def
+#guard_msgs(pass trace, all) in #print sig f_wfrec.induct_unfolding
+
+/-- info: theorem f_exp_wfrec.eq_1 : ∀ (x : Nat), f_exp_wfrec 0 x = x -/
+#guard_msgs(pass trace, all) in
+#print sig f_exp_wfrec.eq_1
 
 /--
-info: f_exp_wfrec.eq_unfold :
-  f_exp_wfrec = fun x x_1 =>
+info: theorem f_exp_wfrec.eq_def : ∀ (x x_1 : Nat),
+  f_exp_wfrec x x_1 =
     match x, x_1 with
     | 0, acc => acc
     | n.succ, acc => f_exp_wfrec n (acc + 1)
 -/
-#guard_msgs(pass trace, all) in
-#check f_exp_wfrec.eq_unfold
+#guard_msgs in #print sig f_exp_wfrec.eq_def
 
 /--
-info: f_exp_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc acc)
-  (case2 : ∀ (n acc : Nat), motive n (acc + 1) (f_exp_wfrec n (acc + 1)) → motive n.succ acc (f_exp_wfrec n (acc + 1)))
-  (a✝ a✝¹ : Nat) : motive a✝ a✝¹ (f_exp_wfrec a✝ a✝¹)
+info: theorem f_exp_wfrec.eq_unfold : f_exp_wfrec = fun x x_1 =>
+  match x, x_1 with
+  | 0, acc => acc
+  | n.succ, acc => f_exp_wfrec n (acc + 1)
 -/
-#guard_msgs(pass trace, all) in
-#check f_exp_wfrec.induct_unfolding
+#guard_msgs(pass trace, all) in #print sig f_exp_wfrec.eq_unfold
+
+/--
+info: theorem f_exp_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat → Prop),
+  (∀ (acc : Nat), motive 0 acc acc) →
+    (∀ (n acc : Nat), motive n (acc + 1) (f_exp_wfrec n (acc + 1)) → motive n.succ acc (f_exp_wfrec n (acc + 1))) →
+      ∀ (a a_1 : Nat), motive a a_1 (f_exp_wfrec a a_1)
+-/
+#guard_msgs(pass trace, all) in #print sig f_exp_wfrec.induct_unfolding