Documentation

Init.Data.Range.Polymorphic.Char

source
@[implicit_reducible]
instance Char.instUpwardEnumerable :
Std.PRange.UpwardEnumerable Char
source
@[simp]
theorem Char.pRangeSucc?_eq :
Std.PRange.succ? = succ?
source
@[simp]
theorem Char.pRangeSuccMany?_eq :
Std.PRange.succMany? = succMany?
source
@[implicit_reducible]
instance Char.instHasSize :
Std.Rxc.HasSize Char
source
@[implicit_reducible]
instance Char.instHasSize_1 :
Std.Rxo.HasSize Char
source
@[implicit_reducible]
instance Char.instHasSize_2 :
Std.Rxi.HasSize Char
source
@[implicit_reducible]
instance Char.instLeast? :
Std.PRange.Least? Char
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