Documentation

Init.Data.String.OrderInstances

Register string positions with grind. #

source
def String.Internal.tacticOrder :
Lean.ParserDescr
Equations
Instances For
    source
    instance String.Pos.Raw.instTotalLe :
    Std.Total fun (x1 x2 : Raw) => x1 ≤ x2
    source
    @[instance_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
    source
    instance String.Pos.Raw.instAntisymmLe :
    Std.Antisymm fun (x1 x2 : Raw) => x1 ≤ x2
    source
    instance String.Pos.Raw.instLawfulOrderBEq :
    Std.LawfulOrderBEq Raw
    source
    instance String.Pos.Raw.instLawfulOrderLT :
    Std.LawfulOrderLT Raw
    source
    @[instance_reducible]
    instance String.Pos.Raw.instLinearOrderPackage :
    Std.LinearOrderPackage Raw
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem String.Pos.offset_byteIdx_le_utf8ByteSize (s : String) (p : s.Pos) :
    p.offset.byteIdx ≤ s.utf8ByteSize

    Range fact for grind: positions are bounded by the string size.

    source
    instance String.Pos.instTotalLe {s : String} :
    Std.Total fun (x1 x2 : s.Pos) => x1 ≤ x2
    source
    @[instance_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
    source
    instance String.Pos.instAntisymmLe {s : String} :
    Std.Antisymm fun (x1 x2 : s.Pos) => x1 ≤ x2
    source
    instance String.Pos.instLawfulOrderBEq {s : String} :
    Std.LawfulOrderBEq s.Pos
    source
    instance String.Pos.instLawfulOrderLT {s : String} :
    Std.LawfulOrderLT s.Pos
    source
    @[instance_reducible]
    instance String.Pos.instLinearOrderPackage {s : String} :
    Std.LinearOrderPackage s.Pos
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem String.Slice.Pos.offset_byteIdx_le_utf8ByteSize (s : Slice) (p : s.Pos) :
    p.offset.byteIdx ≤ s.utf8ByteSize

    Range fact for grind: positions are bounded by the slice size.

    source
    instance String.Slice.Pos.instTotalLe {s : Slice} :
    Std.Total fun (x1 x2 : s.Pos) => x1 ≤ x2
    source
    @[instance_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
    source
    instance String.Slice.Pos.instAntisymmLe {s : Slice} :
    Std.Antisymm fun (x1 x2 : s.Pos) => x1 ≤ x2
    source
    instance String.Slice.Pos.instLawfulOrderBEq {s : Slice} :
    Std.LawfulOrderBEq s.Pos
    source
    instance String.Slice.Pos.instLawfulOrderLT {s : Slice} :
    Std.LawfulOrderLT s.Pos
    source
    @[instance_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.