Documentation

Lean.Data.Position

structure Lean.Position :
Instances For
    Equations
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      Equations
      structure Lean.FileMap :
      Instances For
        Equations
        class Lean.MonadFileMap (m : TypeType) :
        Instances
          partial def Lean.FileMap.ofString.loop (s : String) (i : String.Pos) (line : Nat) (ps : Array String.Pos) (lines : Array Nat) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            partial def Lean.FileMap.toPosition.loop (pos : String.Pos) (str : String) (ps : Array String.Pos) (lines : Array Nat) (b : Nat) (e : Nat) :