Idris2Doc : Data.Nat.Exponentiation

Data.Nat.Exponentiation

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