Documentation

Init.MetaTypes

Equations
structure Lean.Module :

Syntax objects for a Lean module.

Instances For
Instances For

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.

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

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

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.

  • 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

    This option does not have any effect (yet).

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

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.