Documentation
Init
.
Data
.
Nat
.
Power2
Search
return to top
source
Imports
Init.Data.Nat.Linear
Imported by
Init.Data.Nat
Lean.Data.HashMap
Init.Data.Nat.Lemmas
Init.Data.BitVec.Basic
Lean.Data.HashSet
Nat
.
nextPowerOfTwo_dec
Nat
.
nextPowerOfTwo
Nat
.
nextPowerOfTwo
.
go
Nat
.
isPowerOfTwo
Nat
.
one_isPowerOfTwo
Nat
.
mul2_isPowerOfTwo_of_isPowerOfTwo
Nat
.
pos_of_isPowerOfTwo
Nat
.
isPowerOfTwo_nextPowerOfTwo
Nat
.
isPowerOfTwo_nextPowerOfTwo
.
isPowerOfTwo_go
source
theorem
Nat
.
nextPowerOfTwo_dec
{n power :
Nat
}
(h₁ :
power
>
0
)
(h₂ :
power
<
n
)
:
n
-
power
*
2
<
n
-
power
source
def
Nat
.
nextPowerOfTwo
(n :
Nat
)
:
Nat
Equations
n
.
nextPowerOfTwo
=
Nat.nextPowerOfTwo.go
n
1
Nat.nextPowerOfTwo.proof_1
source
@[irreducible]
def
Nat
.
nextPowerOfTwo
.
go
(n power :
Nat
)
(h :
power
>
0
)
:
Nat
Equations
Nat.nextPowerOfTwo.go
n
power
h
=
if
power
<
n
then
Nat.nextPowerOfTwo.go
n
(
power
*
2
)
⋯
else
power
source
def
Nat
.
isPowerOfTwo
(n :
Nat
)
:
Prop
Equations
n
.
isPowerOfTwo
=
∃
(
k
:
Nat
)
,
n
=
2
^
k
source
theorem
Nat
.
one_isPowerOfTwo
:
isPowerOfTwo
1
source
theorem
Nat
.
mul2_isPowerOfTwo_of_isPowerOfTwo
{n :
Nat
}
(h :
n
.
isPowerOfTwo
)
:
(
n
*
2
).
isPowerOfTwo
source
theorem
Nat
.
pos_of_isPowerOfTwo
{n :
Nat
}
(h :
n
.
isPowerOfTwo
)
:
n
>
0
source
theorem
Nat
.
isPowerOfTwo_nextPowerOfTwo
(n :
Nat
)
:
n
.
nextPowerOfTwo
.
isPowerOfTwo
source
@[irreducible]
theorem
Nat
.
isPowerOfTwo_nextPowerOfTwo
.
isPowerOfTwo_go
(n power :
Nat
)
(h₁ :
power
>
0
)
(h₂ :
power
.
isPowerOfTwo
)
:
(
nextPowerOfTwo.go
n
power
h₁
)
.
isPowerOfTwo