Idris2Doc : Data.Nat.Exponentiation

Data.Nat.Exponentiation

lpow : Nat -> Nat -> Nat
  Totality: total
lpow2 : Nat -> Nat
  Totality: total
lteLpow2 : LTE 1 (lpow2 m)
  Totality: total
ltePow2 : LTE 1 (pow2 m)
  Totality: total
modularCorrect : (v : Nat) -> pow v n = lpow v n
  Totality: total
pow : Nat -> Nat -> Nat
  Totality: total
pow2 : Nat -> Nat
  Totality: total
pow2Correct : pow2 n = lpow2 n
  Totality: total
pow2Increasing : LT (pow2 m) (pow2 (S m))
  Totality: total
unfoldLpow2 : lpow2 (S n) = lpow2 n + lpow2 n
  Totality: total
unfoldPow2 : pow2 (S n) = pow2 n + pow2 n
  Totality: total