Documentation
Mathlib
.
Init
.
ZeroOne
Search
Google site search
Mathlib
.
Init
.
ZeroOne
source
Imports
Init
Mathlib.Mathport.Rename
Mathlib.Tactic.ToAdditive
Imported by
Zero
Zero
.
toOfNat0
Zero
.
ofOfNat0
One
One
.
toOfNat1
One
.
ofOfNat1
bit0
bit1
Classes for
Zero
and
One
#
source
class
Zero
(α :
Type
u)
:
Type
u
zero :
α
Instances
source
instance
Zero
.
toOfNat0
{α :
Type
u_1}
[
Zero
α
]
:
OfNat
α
0
source
instance
Zero
.
ofOfNat0
{α :
Type
u_1}
[
OfNat
α
0
]
:
Zero
α
source
class
One
(α :
Type
u)
:
Type
u
one :
α
Instances
source
instance
One
.
toOfNat1
{α :
Type
u_1}
[
One
α
]
:
OfNat
α
1
source
instance
One
.
ofOfNat1
{α :
Type
u_1}
[
OfNat
α
1
]
:
One
α
source
@[match_pattern, deprecated]
def
bit0
{α :
Type
u}
[
Add
α
]
(a :
α
)
:
α
Instances For
source
@[match_pattern, deprecated]
def
bit1
{α :
Type
u}
[
One
α
]
[
Add
α
]
(a :
α
)
:
α
Instances For