Idris2Doc : Data.Monoid.Exponentiation

Data.Monoid.Exponentiation

(^) : Numa => a -> Nat -> a
Totality: total
Fixity Declaration: infixr operator, level 10
linear : Monoida => a -> Nat -> a
Totality: total
linearPlusHomo : {automon : Monoida} -> (x<+>y) <+>z = x<+> (y<+>z) -> neutral<+>x = x -> (v : a) -> linearvm<+>linearvn = linearv (m+n)
Totality: total
modular : Monoida => a -> Nat -> a
Totality: total
modularCorrect : {automon : Monoida} -> (x<+>y) <+>z = x<+> (y<+>z) -> neutral<+>x = x -> (v : a) -> modularvn = linearvn
Totality: total
modularRec : Monoida => a -> HalfRecn -> a
Totality: total
modularRecCorrect : {automon : Monoida} -> (x<+>y) <+>z = x<+> (y<+>z) -> neutral<+>x = x -> (v : a) -> (p : HalfRecn) -> modularRecvp = linearvn
Totality: total