Documentation

Lean.Elab.Calc

Decompose e into (r, a, b).

Remark: it assumes the last two arguments are explicit.

Instances For
    def Lean.Elab.Term.mkCalcTrans (result : Lean.Expr) (resultType : Lean.Expr) (step : Lean.Expr) (stepType : Lean.Expr) :
    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 futher 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
      Instances For
        Instances For
          Instances For

            Elaborator for the calc term mode variant.

            Instances For