Register string positions with grind.

def String.Internal.tacticOrder : Lean.ParserDescr

Equations

• String.Internal.tacticOrder = Lean.ParserDescr.node `String.Internal.tacticOrder 1024 (Lean.ParserDescr.nonReservedSymbol "order" false)

@[instance_reducible]

instance String.Pos.Raw.instToIntCiOfNatInt : Lean.Grind.ToInt Raw (Lean.Grind.IntInterval.ci 0)

Equations

• String.Pos.Raw.instToIntCiOfNatInt = { toInt := fun (p : String.Pos.Raw) => ↑p.byteIdx, toInt_inj := ⋯, toInt_mem := String.Pos.Raw.instToIntCiOfNatInt._proof_4 }

@[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_reducible]

instance String.Pos.instToIntCoOfNatIntHAddCastUtf8ByteSize {s : String} : Lean.Grind.ToInt s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))

Equations

• String.Pos.instToIntCoOfNatIntHAddCastUtf8ByteSize = { toInt := fun (p : s.Pos) => ↑p.offset.byteIdx, toInt_inj := ⋯, toInt_mem := ⋯ }

@[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_reducible]

instance String.Slice.Pos.instToIntCoOfNatIntHAddCastUtf8ByteSize {s : Slice} : Lean.Grind.ToInt s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))

Equations

• String.Slice.Pos.instToIntCoOfNatIntHAddCastUtf8ByteSize = { toInt := fun (p : s.Pos) => ↑p.offset.byteIdx, toInt_inj := ⋯, toInt_mem := ⋯ }

@[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