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

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.

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

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

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.

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.

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

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

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

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

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

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

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

When true (default: false), unfolds definitions. This can be enabled using the simp! syntax.

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.

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

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.

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.

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.

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

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

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.

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

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.

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

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.

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.

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

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

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

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

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

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

When true (default: false), unfolds definitions. This can be enabled using the simp! syntax.

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

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.

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.

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

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.

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.