structure Lean.NameGenerator : Type

• namePrefix : Name
• idx : Nat

@[implicit_reducible]

instance Lean.instInhabitedNameGenerator : Inhabited NameGenerator

Equations

• Lean.instInhabitedNameGenerator = { default := Lean.instInhabitedNameGenerator.default }

def Lean.instInhabitedNameGenerator.default : NameGenerator

Equations

• Lean.instInhabitedNameGenerator.default = { namePrefix := default, idx := default }

structure Lean.Module : Type

Syntax objects for a Lean module.

• header : Syntax
• commands : Array Syntax

inductive Lean.Meta.TransparencyMode : Type

Controls which constants isDefEq (definitional equality) and whnf (weak head normal form) are allowed to unfold.

Background: "try-hard" vs "speculative" modes

During type checking of user input, we assume the input is most likely correct, and we want Lean to try hard before reporting a failure. Here, it is fine to unfold [semireducible] definitions (the .default setting).

During proof automation (simp, rw, type class resolution), we perform many speculative isDefEq calls — most of which fail. In this setting, we do not want to try hard: unfolding too many definitions is a performance footgun. This is why .reducible exists.

The transparency hierarchy

The levels form a linear order: none < reducible < instances < default < all. Each level unfolds everything the previous level does, plus more:

• reducible: Only unfolds [reducible] definitions. Used for speculative isDefEq checks (e.g., discrimination tree lookups in simp, type class resolution). Think of [reducible] as [inline] for type checking and indexing.

• instances: Also unfolds [implicit_reducible] definitions. Instance diamonds are common: for example, Add Nat can come from a direct instance or via Semiring. These instances are all definitionally equal but structurally different, so isDefEq must unfold them to confirm equality. This level also handles definitions used in types that appear in implicit arguments (e.g., Nat.add, Array.size). However, these definitions must not be eagerly reduced (instances become huge terms), and discrimination trees do not index them. This makes .instances safe for speculative checks involving implicit arguments without the performance cost of .default.

• default: Also unfolds [semireducible] definitions (anything not [irreducible]). Used for type checking user input where we want to try hard.

• all: Also unfolds [irreducible] definitions. Rarely used.

Implicit arguments and transparency

When proof automation (e.g., simp, rw) applies a lemma, explicit arguments are checked at the caller's transparency (typically .reducible). But implicit arguments are often "invisible" to the user — if a lemma fails to apply because of an implicit argument mismatch, the user is confused. Historically, Lean bumped transparency to .default for implicit arguments, but this eventually became a performance bottleneck in Mathlib. The option backward.isDefEq.respectTransparency (default: true) disables this bump. Instead, instance-implicit arguments ([..]) are checked at .instances, and other implicit arguments are checked at the caller's transparency.

See also: ReducibilityStatus, backward.isDefEq.respectTransparency, backward.whnf.reducibleClassField.

• all : TransparencyMode

  Unfolds all constants, even those tagged as @[irreducible].

• default : TransparencyMode

  Unfolds all constants except those tagged as @[irreducible]. Used for type checking user-written terms where we expect the input to be correct and want to try hard.

• reducible : TransparencyMode

  Unfolds only constants tagged with the @[reducible] attribute. Used for speculative isDefEq in proof automation (simp, rw, type class resolution) where most checks fail and we must not try too hard.

• instances : TransparencyMode

  Unfolds reducible constants and constants tagged with @[implicit_reducible]. Used for checking implicit arguments during proof automation, and for unfolding class projections applied to instances. Instance diamonds (e.g., Add Nat from a direct instance vs from Semiring) are definitionally equal but structurally different, so isDefEq must unfold them. Also handles definitions used in types of implicit arguments (e.g., Nat.add, Array.size).

• none : TransparencyMode

  Do not unfold anything.

@[implicit_reducible]

instance Lean.Meta.instInhabitedTransparencyMode : Inhabited TransparencyMode

Equations

• Lean.Meta.instInhabitedTransparencyMode = { default := Lean.Meta.instInhabitedTransparencyMode.default }

def Lean.Meta.instInhabitedTransparencyMode.default : TransparencyMode

Equations

• Lean.Meta.instInhabitedTransparencyMode.default = Lean.Meta.TransparencyMode.all

def Lean.Meta.instBEqTransparencyMode.beq : TransparencyMode → TransparencyMode → Bool

Equations

• Lean.Meta.instBEqTransparencyMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Lean.Meta.instBEqTransparencyMode : BEq TransparencyMode

Equations

• Lean.Meta.instBEqTransparencyMode = { beq := Lean.Meta.instBEqTransparencyMode.beq }

inductive Lean.Meta.EtaStructMode : Type

Which structure types should eta be used with?

• all : EtaStructMode

  Enable eta for structure and classes.

• notClasses : EtaStructMode

  Enable eta only for structures that are not classes.

• none : EtaStructMode

  Disable eta for structures and classes.

@[implicit_reducible]

instance Lean.Meta.instInhabitedEtaStructMode : Inhabited EtaStructMode

Equations

• Lean.Meta.instInhabitedEtaStructMode = { default := Lean.Meta.instInhabitedEtaStructMode.default }

def Lean.Meta.instInhabitedEtaStructMode.default : EtaStructMode

Equations

• Lean.Meta.instInhabitedEtaStructMode.default = Lean.Meta.EtaStructMode.all

def Lean.Meta.instBEqEtaStructMode.beq : EtaStructMode → EtaStructMode → Bool

Equations

• Lean.Meta.instBEqEtaStructMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Lean.Meta.instBEqEtaStructMode : BEq EtaStructMode

Equations

• Lean.Meta.instBEqEtaStructMode = { beq := Lean.Meta.instBEqEtaStructMode.beq }

structure Lean.Meta.DSimp.Config : Type

The configuration for dsimp. Passed to dsimp using, for example, the dsimp (config := {zeta := false}) syntax.

Implementation note: this structure is only used for processing the (config := ...) syntax, and it is not used internally. It is immediately converted to Lean.Meta.Simp.Config by Lean.Elab.Tactic.elabSimpConfig.

• zeta : Bool

  When true (default: true), performs zeta reduction of let and have expressions. That is, let x := v; e[x] reduces to e[v]. If zetaHave is false then have expressions are not zeta reduced. See also zetaDelta.

• beta : Bool

  When true (default: true), performs beta reduction of applications of fun expressions. That is, (fun x => e[x]) v reduces to e[v].

• eta : Bool

  TODO (currently unimplemented). When true (default: true), performs eta reduction for fun expressions. That is, (fun x => f x) reduces to f.

• etaStruct : EtaStructMode

  Configures how to determine definitional equality between two structure instances. See documentation for Lean.Meta.EtaStructMode.

• iota : Bool

  When true (default: true), reduces match expressions applied to constructors.

• proj : Bool

  When true (default: true), reduces projections of structure constructors.

• decide : Bool

  When true (default: false), rewrites a proposition p to True or False by inferring a Decidable p instance and reducing it.

• autoUnfold : Bool

  When true (default: false), unfolds applications of functions defined by pattern matching, when one of the patterns applies. This can be enabled using the simp! syntax.

• failIfUnchanged : Bool

  If failIfUnchanged is true (default: true), then calls to simp, dsimp, or simp_all will fail if they do not make progress.

• unfoldPartialApp : Bool

  If unfoldPartialApp is true (default: false), then calls to simp, dsimp, or simp_all will unfold even partial applications of f when we request f to be unfolded.

• zetaDelta : Bool

  When true (default: false), local definitions are unfolded. That is, given a local context containing x : t := e, then the free variable x reduces to e. Otherwise, x must be provided as a simp argument.

• index : Bool

  When index (default : true) is false, simp will only use the root symbol to find candidate simp theorems. It approximates Lean 3 simp behavior.

• zetaUnused : Bool

  When true (default : true), then simp will remove unused let and have expressions: let x := v; e simplifies to e when x does not occur in e.

• zetaHave : Bool

  When false (default: true), then disables zeta reduction of have expressions. If zeta is false, then this option has no effect. Unused haves are still removed if zeta or zetaUnused are true.

• locals : Bool

  If locals is true, dsimp will unfold all definitions from the current file. For local theorems, use +suggestions instead.

• instances : Bool

  If instances is true, dsimp will visit instance arguments. If option backward.dsimp.instances is true, it overrides this field.

@[implicit_reducible]

instance Lean.Meta.DSimp.instInhabitedConfig : Inhabited Config

Equations

• Lean.Meta.DSimp.instInhabitedConfig = { default := Lean.Meta.DSimp.instInhabitedConfig.default }

def Lean.Meta.DSimp.instInhabitedConfig.default : Config

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.DSimp.instBEqConfig.beq : Config → Config → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.DSimp.instBEqConfig.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Lean.Meta.DSimp.instBEqConfig : BEq Config

Equations

• Lean.Meta.DSimp.instBEqConfig = { beq := Lean.Meta.DSimp.instBEqConfig.beq }

@[inline]

def Lean.Meta.Simp.defaultMaxSteps : Nat

Equations

• Lean.Meta.Simp.defaultMaxSteps = 100000

structure Lean.Meta.Simp.Config : Type

The configuration for simp. Passed to simp using, for example, the simp +contextual or simp (maxSteps := 100000) syntax.

See also Lean.Meta.Simp.neutralConfig and Lean.Meta.DSimp.Config.

• maxSteps : Nat

  The maximum number of subexpressions to visit when performing simplification. The default is 100000.

• maxDischargeDepth : Nat

  When simp discharges side conditions for conditional lemmas, it can recursively apply simplification. The maxDischargeDepth (default: 2) is the maximum recursion depth when recursively applying simplification to side conditions.

• contextual : Bool

  When contextual is true (default: false) and simplification encounters an implication p → q it includes p as an additional simp lemma when simplifying q.

• memoize : Bool

  When true (default: true) then the simplifier caches the result of simplifying each sub-expression, if possible.

• singlePass : Bool

  When singlePass is true (default: false), the simplifier runs through a single round of simplification, which consists of running pre-methods, recursing using congruence lemmas, and then running post-methods. Otherwise, when it is false, it iteratively applies this simplification procedure.

• zeta : Bool

  When true (default: true), performs zeta reduction of let and have expressions. That is, let x := v; e[x] reduces to e[v]. If zetaHave is false then have expressions are not zeta reduced. See also zetaDelta.

• beta : Bool

  When true (default: true), performs beta reduction of applications of fun expressions. That is, (fun x => e[x]) v reduces to e[v].

• eta : Bool

  TODO (currently unimplemented). When true (default: true), performs eta reduction for fun expressions. That is, (fun x => f x) reduces to f.

• etaStruct : EtaStructMode

  Configures how to determine definitional equality between two structure instances. See documentation for Lean.Meta.EtaStructMode.

• iota : Bool

  When true (default: true), reduces match expressions applied to constructors.

• proj : Bool

  When true (default: true), reduces projections of structure constructors.

• decide : Bool

  When true (default: false), rewrites a proposition p to True or False by inferring a Decidable p instance and reducing it.

• arith : Bool

  When true (default: false), simplifies simple arithmetic expressions.

• autoUnfold : Bool

  When true (default: false), unfolds applications of functions defined by pattern matching, when one of the patterns applies. This can be enabled using the simp! syntax.

• dsimp : Bool

  When true (default: true) then switches to dsimp on dependent arguments if there is no congruence theorem that would allow simp to visit them. When dsimp is false, then the argument is not visited.

• failIfUnchanged : Bool

  If failIfUnchanged is true (default: true), then calls to simp, dsimp, or simp_all will fail if they do not make progress.

• ground : Bool

  If ground is true (default: false), then ground terms are reduced. A term is ground when it does not contain free or meta variables. Reduction is interrupted at a function application f ... if f is marked to not be unfolded. Ground term reduction applies @[seval] lemmas.

• unfoldPartialApp : Bool

  If unfoldPartialApp is true (default: false), then calls to simp, dsimp, or simp_all will unfold even partial applications of f when we request f to be unfolded.

• zetaDelta : Bool

  When true (default: false), local definitions are unfolded. That is, given a local context containing x : t := e, then the free variable x reduces to e. Otherwise, x must be provided as a simp argument.

• index : Bool

  When index (default : true) is false, simp will only use the root symbol to find candidate simp theorems. It approximates Lean 3 simp behavior.

• implicitDefEqProofs : Bool

  If implicitDefEqProofs := true, simp does not create proof terms when the input and output terms are definitionally equal.

• zetaUnused : Bool

  When true (default : true), then simp removes unused let and have expressions: let x := v; e simplifies to e when x does not occur in e. This option takes precedence over zeta and zetaHave.

• catchRuntime : Bool

  When true (default : true), then simp catches runtime exceptions and converts them into simp exceptions.

• zetaHave : Bool

  When false (default: true), then disables zeta reduction of have expressions. If zeta is false, then this option has no effect. Unused haves are still removed if zeta or zetaUnused are true.

• letToHave : Bool

  When true (default : true), then simp will attempt to transform lets into haves if they are non-dependent. This only applies when zeta := false.

• congrConsts : Bool

  When true (default: true), simp tries to realize constant f.congr_simp when constructing an auxiliary congruence proof for f. This option exists because the termination prover uses simp and withoutModifyingEnv while constructing the termination proof. Thus, any constant realized by simp is deleted.

• bitVecOfNat : Bool

  When true (default: true), the bitvector simprocs use BitVec.ofNat for representing bitvector literals.

• warnExponents : Bool

  When true (default: true), the ^ simprocs generate an warning it the exponents are too big.

• suggestions : Bool

  If suggestions is true, simp? will invoke the currently configured library suggestion engine on the current goal, and attempt to use the resulting suggestions as parameters to the simp tactic.

• maxSuggestions : Option Nat

  Maximum number of library suggestions to use. If none, uses the default limit. Only relevant when suggestions is true.

• locals : Bool

  If locals is true, simp will unfold all definitions from the current file. For local theorems, use +suggestions instead.

• instances : Bool

  If instances is true, simp will visit instance arguments. If option backward.dsimp.instances is true, it overrides this field.

def Lean.Meta.Simp.instInhabitedConfig.default : Config

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Meta.Simp.instInhabitedConfig : Inhabited Config

Equations

• Lean.Meta.Simp.instInhabitedConfig = { default := Lean.Meta.Simp.instInhabitedConfig.default }

def Lean.Meta.Simp.instBEqConfig.beq : Config → Config → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Simp.instBEqConfig.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Lean.Meta.Simp.instBEqConfig : BEq Config

Equations

• Lean.Meta.Simp.instBEqConfig = { beq := Lean.Meta.Simp.instBEqConfig.beq }

structure Lean.Meta.Simp.ConfigCtxextends Lean.Meta.Simp.Config : Type

• maxSteps : Nat
• maxDischargeDepth : Nat
• contextual : Bool
• memoize : Bool
• singlePass : Bool
• zeta : Bool
• beta : Bool
• eta : Bool
• etaStruct : EtaStructMode
• iota : Bool
• proj : Bool
• decide : Bool
• arith : Bool
• autoUnfold : Bool
• dsimp : Bool
• failIfUnchanged : Bool
• ground : Bool
• unfoldPartialApp : Bool
• zetaDelta : Bool
• index : Bool
• implicitDefEqProofs : Bool
• zetaUnused : Bool
• catchRuntime : Bool
• zetaHave : Bool
• letToHave : Bool
• congrConsts : Bool
• bitVecOfNat : Bool
• warnExponents : Bool
• suggestions : Bool
• maxSuggestions : Option Nat
• locals : Bool
• instances : Bool

def Lean.Meta.Simp.neutralConfig : Config

A neutral configuration for simp, turning off all reductions and other built-in simplifications.

Equations

• Lean.Meta.Simp.neutralConfig = { zeta := false, beta := false, eta := false, iota := false, proj := false, zetaUnused := false, letToHave := false }

structure Lean.Meta.Simp.NormCastConfigextends Lean.Meta.Simp.Config : Type

• maxSteps : Nat
• maxDischargeDepth : Nat
• contextual : Bool
• memoize : Bool
• singlePass : Bool
• zeta : Bool
• beta : Bool
• eta : Bool
• etaStruct : EtaStructMode
• iota : Bool
• proj : Bool
• decide : Bool
• arith : Bool
• autoUnfold : Bool
• dsimp : Bool
• failIfUnchanged : Bool
• ground : Bool
• unfoldPartialApp : Bool
• zetaDelta : Bool
• index : Bool
• implicitDefEqProofs : Bool
• zetaUnused : Bool
• catchRuntime : Bool
• zetaHave : Bool
• letToHave : Bool
• congrConsts : Bool
• bitVecOfNat : Bool
• warnExponents : Bool
• suggestions : Bool
• maxSuggestions : Option Nat
• locals : Bool
• instances : Bool

inductive Lean.Meta.Occurrences : Type

Configuration for which occurrences that match an expression should be rewritten.

• all : Occurrences

  All occurrences should be rewritten.

• pos (idxs : List Nat) : Occurrences

  A list of indices for which occurrences should be rewritten.

• neg (idxs : List Nat) : Occurrences

  A list of indices for which occurrences should not be rewritten.

@[implicit_reducible]

instance Lean.Meta.instInhabitedOccurrences : Inhabited Occurrences

Equations

• Lean.Meta.instInhabitedOccurrences = { default := Lean.Meta.instInhabitedOccurrences.default }

def Lean.Meta.instInhabitedOccurrences.default : Occurrences

Equations

• Lean.Meta.instInhabitedOccurrences.default = Lean.Meta.Occurrences.all

@[implicit_reducible]

instance Lean.Meta.instBEqOccurrences : BEq Occurrences

Equations

• Lean.Meta.instBEqOccurrences = { beq := Lean.Meta.instBEqOccurrences.beq }

def Lean.Meta.instBEqOccurrences.beq : Occurrences → Occurrences → Bool

Equations

• Lean.Meta.instBEqOccurrences.beq Lean.Meta.Occurrences.all Lean.Meta.Occurrences.all = true
• Lean.Meta.instBEqOccurrences.beq (Lean.Meta.Occurrences.pos a) (Lean.Meta.Occurrences.pos b) = (a == b)
• Lean.Meta.instBEqOccurrences.beq (Lean.Meta.Occurrences.neg a) (Lean.Meta.Occurrences.neg b) = (a == b)
• Lean.Meta.instBEqOccurrences.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Lean.Meta.instCoeListNatOccurrences : Coe (List Nat) Occurrences

Equations

• Lean.Meta.instCoeListNatOccurrences = { coe := Lean.Meta.Occurrences.pos }

structure Lean.Meta.ExtractLetsConfig : Type

Configuration for the extract_lets tactic.

• proofs : Bool

  If true (default: false), extract lets from subterms that are proofs. Top-level lets are always extracted.

• types : Bool

  If true (default: true), extract lets from subterms that are types. Top-level lets are always extracted.

• implicits : Bool

  If true (default: false), extract lets from subterms that are implicit arguments.

• descend : Bool

  If false (default: true), extracts only top-level lets, otherwise allows descending into subterms. When false, proofs and types are ignored, and lets appearing in the types or values of the top-level lets are not themselves extracted.

• underBinder : Bool

  If true (default: true), descend into forall/lambda/let bodies when extracting. Only relevant when descend is true.

• usedOnly : Bool

  If true (default: false), eliminate unused lets rather than extract them.

• merge : Bool

  If true (default: true), reuse local declarations that have syntactically equal values. Note that even when false, the caching strategy for extract_lets may result in fewer extracted let bindings than expected.

• useContext : Bool

  When merging is enabled, if true (default: true), make use of pre-existing local definitions in the local context.

• onlyGivenNames : Bool

  If true (default: false), then once givenNames is exhausted, stop extracting lets. Otherwise continue extracting lets.

• preserveBinderNames : Bool

  If true (default: false), then when no name is provided for a 'let' expression, the name is used as-is without making it be inaccessible. The name still might be inaccessible if the binder name was.

• lift : Bool

  If true (default: false), lift non-extractable lets as far out as possible.

structure Lean.Meta.LiftLetsConfigextends Lean.Meta.ExtractLetsConfig : Type

Configuration for the lift_lets tactic.

• proofs : Bool
• types : Bool
• implicits : Bool
• descend : Bool
• underBinder : Bool
• usedOnly : Bool
• merge : Bool
• useContext : Bool
• onlyGivenNames : Bool
• preserveBinderNames : Bool
• lift : Bool