structure Lean.NameGenerator : Type

• namePrefix : Name
• idx : Nat

instance Lean.instInhabitedNameGenerator : Inhabited 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

Which constants should be unfolded?

• all : TransparencyMode

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

• default : TransparencyMode

  Unfolds all constants except those tagged as @[irreducible].

• reducible : TransparencyMode

  Unfolds only constants tagged with the @[reducible] attribute.

• instances : TransparencyMode

  Unfolds reducible constants and constants tagged with the @[instance] attribute.

instance Lean.Meta.instInhabitedTransparencyMode : Inhabited TransparencyMode

Equations

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

instance Lean.Meta.instBEqTransparencyMode : BEq TransparencyMode

Equations

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

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.

instance Lean.Meta.instInhabitedEtaStructMode : Inhabited EtaStructMode

Equations

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

instance Lean.Meta.instBEqEtaStructMode : BEq EtaStructMode

Equations

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

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 definitions. 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.

instance Lean.Meta.DSimp.instInhabitedConfig : Inhabited Config

Equations

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

instance Lean.Meta.DSimp.instBEqConfig : BEq Config

Equations

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

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 (config := {contextual := true}) 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 subexpression, 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 definitions. 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 will remove 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 simps will catch runtime exceptions and convert 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.

instance Lean.Meta.Simp.instInhabitedConfig : Inhabited Config

Equations

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

instance Lean.Meta.Simp.instBEqConfig : BEq Config

Equations

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

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

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

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.

instance Lean.Meta.instInhabitedOccurrences : Inhabited Occurrences

Equations

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

instance Lean.Meta.instBEqOccurrences : BEq Occurrences

Equations

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

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