HepLean Documentation
Init
.
Data
.
Char
.
Lemmas
Search
Google site search
return to top
source
Imports
Init.Data.Char.Basic
Init.Data.UInt.Lemmas
Imported by
Char
.
le_def
Char
.
lt_def
Char
.
lt_iff_val_lt_val
Char
.
not_le
Char
.
not_lt
Char
.
le_refl
Char
.
lt_irrefl
Char
.
le_trans
Char
.
lt_trans
Char
.
le_total
Char
.
lt_asymm
Char
.
ne_of_lt
Char
.
utf8Size_eq
Char
.
ofNat_toNat
Char
.
ext
String
.
csize
source
theorem
Char
.
le_def
{a b :
Char
}
:
a
≤
b
↔
a
.val
≤
b
.val
source
theorem
Char
.
lt_def
{a b :
Char
}
:
a
<
b
↔
a
.val
<
b
.val
source
theorem
Char
.
lt_iff_val_lt_val
{a b :
Char
}
:
a
<
b
↔
a
.val
<
b
.val
source
@[simp]
theorem
Char
.
not_le
{a b :
Char
}
:
¬
a
≤
b
↔
b
<
a
source
@[simp]
theorem
Char
.
not_lt
{a b :
Char
}
:
¬
a
<
b
↔
b
≤
a
source
@[simp]
theorem
Char
.
le_refl
(a :
Char
)
:
a
≤
a
source
@[simp]
theorem
Char
.
lt_irrefl
(a :
Char
)
:
¬
a
<
a
source
theorem
Char
.
le_trans
{a b c :
Char
}
:
a
≤
b
→
b
≤
c
→
a
≤
c
source
theorem
Char
.
lt_trans
{a b c :
Char
}
:
a
<
b
→
b
<
c
→
a
<
c
source
theorem
Char
.
le_total
(a b :
Char
)
:
a
≤
b
∨
b
≤
a
source
theorem
Char
.
lt_asymm
{a b :
Char
}
(h :
a
<
b
)
:
¬
b
<
a
source
theorem
Char
.
ne_of_lt
{a b :
Char
}
(h :
a
<
b
)
:
a
≠
b
source
theorem
Char
.
utf8Size_eq
(c :
Char
)
:
c
.utf8Size
=
1
∨
c
.utf8Size
=
2
∨
c
.utf8Size
=
3
∨
c
.utf8Size
=
4
source
@[simp]
theorem
Char
.
ofNat_toNat
(c :
Char
)
:
Char.ofNat
c
.toNat
=
c
source
theorem
Char
.
ext
{a b :
Char
}
:
a
.val
=
b
.val
→
a
=
b
source
@[reducible, inline, deprecated Char.utf8Size]
abbrev
String
.
csize
(c :
Char
)
:
Nat
Equations
String.csize
=
Char.utf8Size
Instances For