Documentation

Init.Data.String.Grind

Register string positions with `grind`. #

def String.Internal.tacticOrder :

Lean.ParserDescr

Equations

Instances For

instance String.Pos.Raw.instToIntCiOfNatInt :

Lean.Grind.ToInt Raw (Lean.Grind.IntInterval.ci 0)

Equations

@[simp]

theorem String.Pos.Raw.toInt_eq {p : Raw} :

↑p = ↑p.byteIdx

instance String.Pos.Raw.instLECiOfNatInt :

Lean.Grind.ToInt.LE Raw (Lean.Grind.IntInterval.ci 0)

instance String.Pos.Raw.instLTCiOfNatInt :

Lean.Grind.ToInt.LT Raw (Lean.Grind.IntInterval.ci 0)

instance String.Pos.Raw.instLawfulOrderLT :

Std.LawfulOrderLT Raw

instance String.Pos.Raw.instIsLinearOrder :

Std.IsLinearOrder Raw

instance String.Pos.instToIntCoOfNatIntHAddCastUtf8ByteSize {s : String} :

Lean.Grind.ToInt s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))

Equations

@[simp]

theorem String.Pos.toInt_eq {s : String} {p : s.Pos} :

↑p = ↑p.offset.byteIdx

instance String.Pos.instLECoOfNatIntHAddCastUtf8ByteSize {s : String} :

Lean.Grind.ToInt.LE s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))

instance String.Pos.instLTCoOfNatIntHAddCastUtf8ByteSize {s : String} :

Lean.Grind.ToInt.LT s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))

instance String.Pos.instLawfulOrderLT {s : String} :

Std.LawfulOrderLT s.Pos

instance String.Pos.instIsLinearOrder {s : String} :

Std.IsLinearOrder s.Pos

instance String.Slice.Pos.instToIntCoOfNatIntHAddCastUtf8ByteSize {s : Slice} :

Lean.Grind.ToInt s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))

Equations

@[simp]

theorem String.Slice.Pos.toInt_eq {s : Slice} {p : s.Pos} :

↑p = ↑p.offset.byteIdx

instance String.Slice.Pos.instLECoOfNatIntHAddCastUtf8ByteSize {s : Slice} :

Lean.Grind.ToInt.LE s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))

instance String.Slice.Pos.instLTCoOfNatIntHAddCastUtf8ByteSize {s : Slice} :

Lean.Grind.ToInt.LT s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))

instance String.Slice.Pos.instLawfulOrderLT {s : Slice} :

Std.LawfulOrderLT s.Pos

instance String.Slice.Pos.instIsLinearOrder {s : Slice} :

Std.IsLinearOrder s.Pos