Documentation

Init.Data.Range.Polymorphic.Char

source
instance Char.instUpwardEnumerable :
Std.PRange.UpwardEnumerable Char
Equations
    source
    @[simp]
    theorem Char.pRangeSucc?_eq :
    Std.PRange.succ? = succ?
    source
    @[simp]
    theorem Char.pRangeSuccMany?_eq :
    Std.PRange.succMany? = succMany?
    source
    instance Char.instHasSize :
    Std.Rxc.HasSize Char
    Equations
      source
      instance Char.instHasSize_1 :
      Std.Rxo.HasSize Char
      Equations
        source
        instance Char.instHasSize_2 :
        Std.Rxi.HasSize Char
        Equations
          source
          instance Char.instLeast? :
          Std.PRange.Least? Char
          Equations
            source
            @[simp]
            theorem Char.least?_eq :
            Std.PRange.least? = some '\x00'
            source
            instance Char.instLawfulUpwardEnumerable :
            Std.PRange.LawfulUpwardEnumerable Char
            source
            instance Char.instLawfulUpwardEnumerableLE :
            Std.PRange.LawfulUpwardEnumerableLE Char
            source
            instance Char.instLawfulUpwardEnumerableLT :
            Std.PRange.LawfulUpwardEnumerableLT Char
            source
            instance Char.instLawfulUpwardEnumerableLeast? :
            Std.PRange.LawfulUpwardEnumerableLeast? Char
            source
            instance Char.instLawfulHasSize :
            Std.Rxc.LawfulHasSize Char
            source
            instance Char.instIsAlwaysFinite :
            Std.Rxc.IsAlwaysFinite Char
            source
            instance Char.instLawfulHasSize_1 :
            Std.Rxo.LawfulHasSize Char
            source
            instance Char.instIsAlwaysFinite_1 :
            Std.Rxo.IsAlwaysFinite Char
            source
            instance Char.instLawfulHasSize_2 :
            Std.Rxi.LawfulHasSize Char
            source
            instance Char.instIsAlwaysFinite_2 :
            Std.Rxi.IsAlwaysFinite Char