Documentation

Lean.Elab.Calc

Decompose e into (r, a, b).

Remark: it assumes the last two arguments are explicit.

Equations
Instances For
    def Lean.Elab.Term.mkCalcTrans (result : Lean.Expr) (resultType : Lean.Expr) (step : Lean.Expr) (stepType : Lean.Expr) :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Adds a type annotation to a hole that occurs immediately at the beginning of the term. This is so that coercions can trigger when elaborating the term. See https://github.com/leanprover/lean4/issues/2040 for further rationale.

      • _ < 3 is annotated
      • (_) < 3 is not, because it occurs after an atom
      • in _ < _ only the first one is annotated
      • _ + 2 < 3 is annotated (not the best heuristic, ideally we'd like to annotate _ + 2)
      • lt _ 3 is not, because it occurs after an identifier
      Equations
      Instances For
        def Lean.Elab.Term.getCalcFirstStep (step0 : Lean.TSyntax `Lean.calcFirstStep) :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Lean.Elab.Term.getCalcSteps (steps : Lean.TSyntax `Lean.calcSteps) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Elaborator for the calc term mode variant.

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