structure Lean.NameGenerator : Type

• namePrefix : Lake.Name
• idx : Nat

instance Lean.instInhabitedNameGenerator : Inhabited Lean.NameGenerator

Equations

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

structure Lean.Module : Type

Syntax objects for a Lean module.

• header : Lean.Syntax
• commands : Array Lean.Syntax

inductive Lean.Meta.TransparencyMode : Type

• all: Lean.Meta.TransparencyMode

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

• default: Lean.Meta.TransparencyMode

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

• reducible: Lean.Meta.TransparencyMode

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

• instances: Lean.Meta.TransparencyMode

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

instance Lean.Meta.instInhabitedTransparencyMode : Inhabited Lean.Meta.TransparencyMode

Equations

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

instance Lean.Meta.instBEqTransparencyMode : BEq Lean.Meta.TransparencyMode

Equations

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

inductive Lean.Meta.EtaStructMode : Type

• all: Lean.Meta.EtaStructMode

  Enable eta for structure and classes.

• notClasses: Lean.Meta.EtaStructMode

  Enable eta only for structures that are not classes.

• none: Lean.Meta.EtaStructMode

  Disable eta for structures and classes.

instance Lean.Meta.instInhabitedEtaStructMode : Inhabited Lean.Meta.EtaStructMode

Equations

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

instance Lean.Meta.instBEqEtaStructMode : BEq Lean.Meta.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 expressions. That is, let x := v; e[x] reduces to e[v]. 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 : Lean.Meta.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 entry x : t := e, the free variable x reduces to e.

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

instance Lean.Meta.DSimp.instInhabitedConfig : Inhabited Lean.Meta.DSimp.Config

Equations

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

instance Lean.Meta.DSimp.instBEqConfig : BEq Lean.Meta.DSimp.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 expressions. That is, let x := v; e[x] reduces to e[v]. 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 : Lean.Meta.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 entry x : t := e, the free variable x reduces to e.

• 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

  When true (default: true), simp will not create a proof for a rewriting rule associated with an rfl-theorem. Rewriting rules are provided by users by annotating theorems with the attribute @[simp]. If the proof of the theorem is just rfl (reflexivity), and implicitDefEqProofs := true, simp will not create a proof term which is an application of the annotated theorem.

instance Lean.Meta.Simp.instInhabitedConfig : Inhabited Lean.Meta.Simp.Config

Equations

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

instance Lean.Meta.Simp.instBEqConfig : BEq Lean.Meta.Simp.Config

Equations

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

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

def Lean.Meta.Simp.neutralConfig : Lean.Meta.Simp.Config

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

Equations

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

inductive Lean.Meta.Occurrences : Type

• all: Lean.Meta.Occurrences
• pos: List Nat → Lean.Meta.Occurrences
• neg: List Nat → Lean.Meta.Occurrences

instance Lean.Meta.instInhabitedOccurrences : Inhabited Lean.Meta.Occurrences

Equations

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

instance Lean.Meta.instBEqOccurrences : BEq Lean.Meta.Occurrences

Equations

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