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
ink
class
Zero
(α :
Type
u)
:
Type
u
zero :
α
Instances
source
ink
instance
Zero
.
toOfNat0
{α :
Type
u_1}
[inst :
Zero
α
]
:
OfNat
α
0
Equations
Zero.toOfNat0
=
{
ofNat
:=
Zero.zero
}
source
ink
instance
Zero
.
ofOfNat0
{α :
Type
u_1}
[inst :
OfNat
α
0
]
:
Zero
α
Equations
Zero.ofOfNat0
=
{
zero
:=
0
}
source
ink
class
One
(α :
Type
u)
:
Type
u
one :
α
Instances
source
ink
instance
One
.
toOfNat1
{α :
Type
u_1}
[inst :
One
α
]
:
OfNat
α
1
Equations
One.toOfNat1
=
{
ofNat
:=
One.one
}
source
ink
instance
One
.
ofOfNat1
{α :
Type
u_1}
[inst :
OfNat
α
1
]
:
One
α
Equations
One.ofOfNat1
=
{
one
:=
1
}
source
ink
@[match_pattern]
def
bit0
{α :
Type
u}
[inst :
Add
α
]
(a :
α
)
:
α
Equations
bit0
a
=
a
+
a
source
ink
@[match_pattern]
def
bit1
{α :
Type
u}
[inst :
One
α
]
[inst :
Add
α
]
(a :
α
)
:
α
Equations
bit1
a
=
bit0
a
+
1