Init.MetaTypes

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.

Instances For

source

instance Lean.Meta.instInhabitedTransparencyMode :

Inhabited TransparencyMode

Equations

source

instance Lean.Meta.instBEqTransparencyMode :

BEq TransparencyMode

Equations

source

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.

Instances For

source

instance Lean.Meta.instInhabitedEtaStructMode :

Inhabited EtaStructMode

Equations

source

instance Lean.Meta.instBEqEtaStructMode :

BEq EtaStructMode

Equations

source

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.

Instances For

source

instance Lean.Meta.DSimp.instInhabitedConfig :

Inhabited Config

Equations

source

instance Lean.Meta.DSimp.instBEqConfig :

BEq Config

Equations

source

def Lean.Meta.Simp.defaultMaxSteps :

Nat

Equations

Instances For

source

structure Lean.Meta.Simp.Config :

Type

The configuration for simp. Passed to simp using, for example, the simp (config := {contextual := true}) syntax.

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.

Instances For

source

instance Lean.Meta.Simp.instInhabitedConfig :

Inhabited Config

Equations

source

instance Lean.Meta.Simp.instBEqConfig :

BEq Config

Equations

source

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

Type

Instances For

source

def Lean.Meta.Simp.neutralConfig :

Config

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

Equations

Instances For

source

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

Type

Instances For

source

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.

Instances For

source

instance Lean.Meta.instInhabitedOccurrences :

Inhabited Occurrences

Equations

source

instance Lean.Meta.instBEqOccurrences :

BEq Occurrences

Equations

source

instance Lean.Meta.instCoeListNatOccurrences :

Coe (List Nat) Occurrences

Equations

source

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.

Instances For

source

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

Type

Configuration for the lift_lets tactic.

Instances For