Documentation

Init.MetaTypes

Instances For
    Equations
    structure Lean.Module :

    Syntax objects for a Lean module.

    Instances For
      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.

          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

              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.

            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.
              Instances For