IdrisDoc: Interfaces.Verified

Interfaces.Verified

interface VerifiedSemigroup 
semigroupOpIsAssociative : VerifiedSemigroup a => (l : a) -> (c : a) -> (r : a) -> l <+> (c <+> r) = l <+> c <+> r
interface VerifiedRingWithUnity 
ringWithUnityIsUnityL : VerifiedRingWithUnity a => (l : a) -> l <.> unity = l
ringWithUnityIsUnityR : VerifiedRingWithUnity a => (r : a) -> unity <.> r = r
interface VerifiedRing 
ringOpIsAssociative : VerifiedRing a => (l : a) -> (c : a) -> (r : a) -> l <.> (c <.> r) = l <.> c <.> r
ringOpIsDistributiveL : VerifiedRing a => (l : a) -> (c : a) -> (r : a) -> l <.> (c <+> r) = l <.> c <+> l <.> r
ringOpIsDistributiveR : VerifiedRing a => (l : a) -> (c : a) -> (r : a) -> (l <+> c) <.> r = l <.> r <+> c <.> r
interface VerifiedMonoid 
monoidNeutralIsNeutralL : VerifiedMonoid a => (l : a) -> l <+> neutral = l
monoidNeutralIsNeutralR : VerifiedMonoid a => (r : a) -> neutral <+> r = r
interface VerifiedMonad 
monadApplicative : VerifiedMonad m => (mf : m (a -> b)) -> (mx : m a) -> mf <*> mx = mf >>= (\f => mx >>= (\x => pure (f x)))
monadLeftIdentity : VerifiedMonad m => (x : a) -> (f : a -> m b) -> pure x >>= f = f x
monadRightIdentity : VerifiedMonad m => (mx : m a) -> mx >>= pure = mx
monadAssociativity : VerifiedMonad m => (mx : m a) -> (f : a -> m b) -> (g : b -> m c) -> mx >>= f >>= g = mx >>= (\x => f x >>= g)
interface VerifiedMeetSemilattice 
meetSemilatticeMeetIsAssociative : VerifiedMeetSemilattice a => (l : a) -> (c : a) -> (r : a) -> meet l (meet c r) = meet (meet l c) r
meetSemilatticeMeetIsCommutative : VerifiedMeetSemilattice a => (l : a) -> (r : a) -> meet l r = meet r l
meetSemilatticeMeetIsIdempotent : VerifiedMeetSemilattice a => (e : a) -> meet e e = e
interface VerifiedJoinSemilattice 
joinSemilatticeJoinIsAssociative : VerifiedJoinSemilattice a => (l : a) -> (c : a) -> (r : a) -> join l (join c r) = join (join l c) r
joinSemilatticeJoinIsCommutative : VerifiedJoinSemilattice a => (l : a) -> (r : a) -> join l r = join r l
joinSemilatticeJoinIsIdempotent : VerifiedJoinSemilattice a => (e : a) -> join e e = e
interface VerifiedGroup 
groupInverseIsInverseL : VerifiedGroup a => (l : a) -> l <+> inverse l = neutral
groupInverseIsInverseR : VerifiedGroup a => (r : a) -> inverse r <+> r = neutral
interface VerifiedFunctor 
functorIdentity : VerifiedFunctor f => (x : f a) -> map id x = id x
functorComposition : VerifiedFunctor f => (x : f a) -> (g1 : a -> b) -> (g2 : b -> c) -> map (g2 . g1) x = (map g2 . map g1) x
interface VerifiedApplicative 
applicativeMap : VerifiedApplicative f => (x : f a) -> (g : a -> b) -> map g x = pure g <*> x
applicativeIdentity : VerifiedApplicative f => (x : f a) -> pure id <*> x = x
applicativeComposition : VerifiedApplicative f => (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) -> pure (.) <*> g2 <*> g1 <*> x = g2 <*> (g1 <*> x)
applicativeHomomorphism : VerifiedApplicative f => (x : a) -> (g : a -> b) -> pure g <*> pure x = pure (g x)
applicativeInterchange : VerifiedApplicative f => (x : a) -> (g : f (a -> b)) -> g <*> pure x = pure (\g' => g' x) <*> g
interface VerifiedAbelianGroup 
abelianGroupOpIsCommutative : VerifiedAbelianGroup a => (l : a) -> (r : a) -> l <+> r = r <+> l
PlusZZSemiV : VerifiedSemigroup ZZ
PlusZZMonoidV : VerifiedMonoid ZZ
PlusNatSemiV : VerifiedSemigroup Nat
PlusNatMonoidV : VerifiedMonoid Nat
MultZZSemiV : VerifiedSemigroup ZZ
MultZZMonoidV : VerifiedMonoid ZZ
MultNatSemiV : VerifiedSemigroup Nat
MultNatMonoidV : VerifiedMonoid Nat