Data.Monoid.Exponentiation

Definitions

linear : Monoid a => a -> Nat -> a

Totality: total
Visibility: public export

modularRec : Monoid a => a -> HalfRec n -> a

Totality: total
Visibility: public export

modular : Monoid a => a -> Nat -> a

Totality: total
Visibility: public export

(^) : Num a => a -> Nat -> a

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 10

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
Visibility: export

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
Visibility: export

modularCorrect : {auto mon : Monoid a} -> (x <+> y) <+> z = x <+> (y <+> z) -> neutral <+> x = x -> (v : a) -> modular v n = linear v n

Totality: total
Visibility: export