Idris2Doc : Data.Nat.Exponentiation

Data.Nat.Exponentiation

lpow : Nat -> Nat -> Nat
Totality: total
lpow2 : Nat -> Nat
Totality: total
lteLpow2 : LTE 1 (lpow2m)
Totality: total
ltePow2 : LTE 1 (pow2m)
Totality: total
modularCorrect : (v : Nat) -> powvn = lpowvn
Totality: total
pow : Nat -> Nat -> Nat
Totality: total
pow2 : Nat -> Nat
Totality: total
pow2Correct : pow2n = lpow2n
Totality: total
pow2Increasing : LT (pow2m) (pow2 (Sm))
Totality: total
unfoldLpow2 : lpow2 (Sn) = lpow2n+lpow2n
Totality: total
unfoldPow2 : pow2 (Sn) = pow2n+pow2n
Totality: total