Documentation

Init.MetaTypes

Instances For
    Equations
    structure Lean.Module :

    Syntax objects for a Lean module.

    Instances For
      Instances For
        Instances For
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            • maxSteps : Nat
            • maxDischargeDepth : Nat
            • contextual : Bool
            • memoize : Bool
            • singlePass : Bool
            • zeta : Bool
            • beta : Bool
            • eta : Bool
            • 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.

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