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)

@[implicit_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.instTotalLe : Std.Total fun (x1 x2 : Raw) => x1 ≤ x2

@[implicit_reducible]

instance String.Pos.Raw.instTransLe : Trans (fun (x1 x2 : Raw) => x1 ≤ x2) (fun (x1 x2 : Raw) => x1 ≤ x2) fun (x1 x2 : Raw) => x1 ≤ x2

Equations

• String.Pos.Raw.instTransLe = { trans := ⋯ }

instance String.Pos.Raw.instAntisymmLe : Std.Antisymm fun (x1 x2 : Raw) => x1 ≤ x2

instance String.Pos.Raw.instLawfulOrderBEq : Std.LawfulOrderBEq Raw

instance String.Pos.Raw.instLawfulOrderLT : Std.LawfulOrderLT Raw

@[implicit_reducible]

instance String.Pos.Raw.instLinearOrderPackage : Std.LinearOrderPackage Raw

Equations

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

@[implicit_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.instTotalLe {s : String} : Std.Total fun (x1 x2 : s.Pos) => x1 ≤ x2

@[implicit_reducible]

instance String.Pos.instTransLe {s : String} : Trans (fun (x1 x2 : s.Pos) => x1 ≤ x2) (fun (x1 x2 : s.Pos) => x1 ≤ x2) fun (x1 x2 : s.Pos) => x1 ≤ x2

Equations

• String.Pos.instTransLe = { trans := ⋯ }

instance String.Pos.instAntisymmLe {s : String} : Std.Antisymm fun (x1 x2 : s.Pos) => x1 ≤ x2

instance String.Pos.instLawfulOrderBEq {s : String} : Std.LawfulOrderBEq s.Pos

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

@[implicit_reducible]

instance String.Pos.instLinearOrderPackage {s : String} : Std.LinearOrderPackage s.Pos

Equations

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

@[implicit_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.instTotalLe {s : Slice} : Std.Total fun (x1 x2 : s.Pos) => x1 ≤ x2

@[implicit_reducible]

instance String.Slice.Pos.instTransLe {s : Slice} : Trans (fun (x1 x2 : s.Pos) => x1 ≤ x2) (fun (x1 x2 : s.Pos) => x1 ≤ x2) fun (x1 x2 : s.Pos) => x1 ≤ x2

Equations

• String.Slice.Pos.instTransLe = { trans := ⋯ }

instance String.Slice.Pos.instAntisymmLe {s : Slice} : Std.Antisymm fun (x1 x2 : s.Pos) => x1 ≤ x2

instance String.Slice.Pos.instLawfulOrderBEq {s : Slice} : Std.LawfulOrderBEq s.Pos

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

@[implicit_reducible]

instance String.Slice.Pos.instLinearOrderPackage {s : Slice} : Std.LinearOrderPackage s.Pos

Equations

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