structure StrataDDM.SourceRange : Type

Source location information in the DDM is defined by a range of bytes in a UTF-8 string with the input Line/column information can be constructed from a Lean.FileMap

As an example, in the string "123abc\ndef", the string "abc" has the position {start := 3, stop := 6 } while "def" has the position {start := 7, stop := 10 }.

• start : String.Pos.Raw

  The starting offset of the source range.

• stop : String.Pos.Raw

  One past the end of the range.

def StrataDDM.instDecidableEqSourceRange.decEq (x✝ x✝¹ : SourceRange) : Decidable (x✝ = x✝¹)

Equations

• StrataDDM.instDecidableEqSourceRange.decEq { start := a, stop := a_1 } { start := b, stop := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance StrataDDM.instDecidableEqSourceRange : DecidableEq SourceRange

Equations

• StrataDDM.instDecidableEqSourceRange = StrataDDM.instDecidableEqSourceRange.decEq

@[implicit_reducible]

instance StrataDDM.instInhabitedSourceRange : Inhabited SourceRange

Equations

• StrataDDM.instInhabitedSourceRange = { default := StrataDDM.instInhabitedSourceRange.default }

def StrataDDM.instInhabitedSourceRange.default : SourceRange

Equations

• StrataDDM.instInhabitedSourceRange.default = { start := default, stop := default }

def StrataDDM.instReprSourceRange.repr : SourceRange → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance StrataDDM.instReprSourceRange : Repr SourceRange

Equations

• StrataDDM.instReprSourceRange = { reprPrec := StrataDDM.instReprSourceRange.repr }

def StrataDDM.SourceRange.none : SourceRange

Equations

• StrataDDM.SourceRange.none = { start := 0, stop := 0 }

def StrataDDM.SourceRange.isNone (loc : SourceRange) : Bool

Equations

• loc.isNone = decide (loc.start = 0 ∧ loc.stop = 0)

@[implicit_reducible]

instance StrataDDM.SourceRange.instToFormat : Std.ToFormat SourceRange

Equations

• StrataDDM.SourceRange.instToFormat = { format := fun (fr : StrataDDM.SourceRange) => Std.format fr.start ++ Std.format "-" ++ Std.format fr.stop }

def StrataDDM.SourceRange.format (loc : SourceRange) (path : System.FilePath) (fm : Lean.FileMap) : String

Format a SourceRange as a string using a FileMap for line:column conversion. Renders location information in a format VSCode understands. Returns "path:line:col-col" if on same line, otherwise "path:line:col".

Equations

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