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

• zeta : Bool

  let x := v; e[x] reduces to e[v].

• beta : Bool
• eta : Bool
• etaStruct : Lean.Meta.EtaStructMode
• iota : Bool
• proj : Bool
• decide : Bool
• autoUnfold : Bool
• failIfUnchanged : Bool

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

• unfoldPartialApp : Bool

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

• zetaDelta : Bool

  Given a local context containing entry x : t := e, free variable x reduces to e.

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

• maxSteps : Nat
• maxDischargeDepth : Nat
• contextual : Bool
• memoize : Bool
• singlePass : Bool
• zeta : Bool

  let x := v; e[x] reduces to e[v].

• beta : Bool
• eta : Bool
• etaStruct : Lean.Meta.EtaStructMode
• iota : Bool
• proj : Bool
• decide : Bool
• arith : Bool
• autoUnfold : Bool
• dsimp : Bool

  If dsimp := true, then switches to dsimp on dependent arguments where there is no congruence theorem that allows simp to visit them. If dsimp := false, then argument is not visited.

• failIfUnchanged : Bool

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

• ground : Bool

  If ground := true, 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.

• unfoldPartialApp : Bool

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

• zetaDelta : Bool

  Given a local context containing entry x : t := e, free variable x reduces to e.

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

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✝ }