Idris2Doc : Data.Monoid.Exponentiation

Data.Monoid.Exponentiation

(^) : Num a => a -> Nat -> a
  Totality: total
  Fixity Declaration: infixr operator, level 10
linear : Monoid a => a -> Nat -> a
  Totality: total
linearPlusHomo : {auto mon : Monoid a} -> (x <+> y) <+> z = x <+> (y <+> z) -> neutral <+> x = x -> (v : a) -> linear v m <+> linear v n = linear v (m + n)
  Totality: total
modular : Monoid a => a -> Nat -> a
  Totality: total
modularCorrect : {auto mon : Monoid a} -> (x <+> y) <+> z = x <+> (y <+> z) -> neutral <+> x = x -> (v : a) -> modular v n = linear v n
  Totality: total
modularRec : Monoid a => a -> HalfRec n -> a
  Totality: total
modularRecCorrect : {auto mon : Monoid a} -> (x <+> y) <+> z = x <+> (y <+> z) -> neutral <+> x = x -> (v : a) -> (p : HalfRec n) -> modularRec v p = linear v n
  Totality: total