Idris2Doc : Control.Algebra

Control.Algebra

Definitions

interfaceSemigroupV : Type->Type
Parameters: ty
Constraints: Semigroup ty
Methods:
semigroupOpIsAssociative : (l : ty) -> (c : ty) -> (r : ty) ->l<+> (c<+>r) = (l<+>c) <+>r

Implementation: 
SemigroupVty=>SemigroupV (Identityty)
semigroupOpIsAssociative : {auto__con : SemigroupVty} -> (l : ty) -> (c : ty) -> (r : ty) ->l<+> (c<+>r) = (l<+>c) <+>r
Visibility: public export
interfaceMonoidV : Type->Type
Parameters: ty
Constraints: Monoid ty, SemigroupV ty
Methods:
monoidNeutralIsNeutralL : (l : ty) ->l<+>neutral=l
monoidNeutralIsNeutralR : (r : ty) ->neutral<+>r=r

Implementation: 
MonoidVty=>MonoidV (Identityty)
monoidNeutralIsNeutralL : {auto__con : MonoidVty} -> (l : ty) ->l<+>neutral=l
Visibility: public export
monoidNeutralIsNeutralR : {auto__con : MonoidVty} -> (r : ty) ->neutral<+>r=r
Visibility: public export
interfaceGroup : Type->Type
  Sets equipped with a single binary operation that is associative,
along with a neutral element for that binary operation and
inverses for all elements. Satisfies the following laws:

+ Associativity of `<+>`:
forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+ Neutral for `<+>`:
forall a, a <+> neutral == a
forall a, neutral <+> a == a
+ Inverse for `<+>`:
forall a, a <+> inverse a == neutral
forall a, inverse a <+> a == neutral

Parameters: ty
Constraints: MonoidV ty
Methods:
inverse : ty->ty
groupInverseIsInverseR : (r : ty) ->inverser<+>r=neutral

Implementations:
AbelianGroupty->Groupty
GroupHomomorphismab->Groupa
GroupHomomorphismab->Groupb
Ringty->Groupty
inverse : Groupty=>ty->ty
Visibility: public export
groupInverseIsInverseR : {auto__con : Groupty} -> (r : ty) ->inverser<+>r=neutral
Visibility: public export
interfaceAbelianGroup : Type->Type
  Sets equipped with a single binary operation that is associative
and commutative, along with a neutral element for that binary
operation and inverses for all elements. Satisfies the following
laws:

+ Associativity of `<+>`:
forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+ Commutativity of `<+>`:
forall a b, a <+> b == b <+> a
+ Neutral for `<+>`:
forall a, a <+> neutral == a
forall a, neutral <+> a == a
+ Inverse for `<+>`:
forall a, a <+> inverse a == neutral
forall a, inverse a <+> a == neutral

Parameters: ty
Constraints: Group ty
Methods:
groupOpIsCommutative : (l : ty) -> (r : ty) ->l<+>r=r<+>l
groupOpIsCommutative : {auto__con : AbelianGroupty} -> (l : ty) -> (r : ty) ->l<+>r=r<+>l
Visibility: public export
interfaceGroupHomomorphism : Type->Type->Type
  A homomorphism is a mapping that preserves group structure.

Parameters: a, b
Constraints: Group a, Group b
Methods:
to : a->b
toGroup : (x : a) -> (y : a) ->to (x<+>y) =tox<+>toy
to : GroupHomomorphismab=>a->b
Visibility: public export
toGroup : {auto__con : GroupHomomorphismab} -> (x : a) -> (y : a) ->to (x<+>y) =tox<+>toy
Visibility: public export
interfaceRing : Type->Type
  Sets equipped with two binary operations, one associative and
commutative supplied with a neutral element, and the other
associative, with distributivity laws relating the two operations.
Satisfies the following laws:

+ Associativity of `<+>`:
forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+ Commutativity of `<+>`:
forall a b, a <+> b == b <+> a
+ Neutral for `<+>`:
forall a, a <+> neutral == a
forall a, neutral <+> a == a
+ Inverse for `<+>`:
forall a, a <+> inverse a == neutral
forall a, inverse a <+> a == neutral
+ Associativity of `<.>`:
forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
+ Distributivity of `<.>` and `<+>`:
forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

Parameters: ty
Constraints: Group ty
Methods:
(<.>) : ty->ty->ty
Fixity Declaration: infixl operator, level 7
ringOpIsAssociative : (l : ty) -> (c : ty) -> (r : ty) ->l<.> (c<.>r) = (l<.>c) <.>r
ringOpIsDistributiveL : (l : ty) -> (c : ty) -> (r : ty) ->l<.> (c<+>r) = (l<.>c) <+> (l<.>r)
ringOpIsDistributiveR : (l : ty) -> (c : ty) -> (r : ty) -> (l<+>c) <.>r= (l<.>r) <+> (c<.>r)

Implementation: 
RingWithUnityty->Ringty
(<.>) : Ringty=>ty->ty->ty
Visibility: public export
Fixity Declaration: infixl operator, level 7
ringOpIsAssociative : {auto__con : Ringty} -> (l : ty) -> (c : ty) -> (r : ty) ->l<.> (c<.>r) = (l<.>c) <.>r
Visibility: public export
ringOpIsDistributiveL : {auto__con : Ringty} -> (l : ty) -> (c : ty) -> (r : ty) ->l<.> (c<+>r) = (l<.>c) <+> (l<.>r)
Visibility: public export
ringOpIsDistributiveR : {auto__con : Ringty} -> (l : ty) -> (c : ty) -> (r : ty) -> (l<+>c) <.>r= (l<.>r) <+> (c<.>r)
Visibility: public export
interfaceRingWithUnity : Type->Type
  Sets equipped with two binary operations, one associative and
commutative supplied with a neutral element, and the other
associative supplied with a neutral element, with distributivity
laws relating the two operations. Satisfies the following laws:

+ Associativity of `<+>`:
forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+ Commutativity of `<+>`:
forall a b, a <+> b == b <+> a
+ Neutral for `<+>`:
forall a, a <+> neutral == a
forall a, neutral <+> a == a
+ Inverse for `<+>`:
forall a, a <+> inverse a == neutral
forall a, inverse a <+> a == neutral
+ Associativity of `<.>`:
forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
+ Neutral for `<.>`:
forall a, a <.> unity == a
forall a, unity <.> a == a
+ Distributivity of `<.>` and `<+>`:
forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

Parameters: ty
Constraints: Ring ty
Methods:
unity : ty
unityIsRingIdL : (l : ty) ->l<.>unity=l
unityIsRingIdR : (r : ty) ->unity<.>r=r

Implementation: 
Fieldty->RingWithUnityty
unity : RingWithUnityty=>ty
Visibility: public export
unityIsRingIdL : {auto__con : RingWithUnityty} -> (l : ty) ->l<.>unity=l
Visibility: public export
unityIsRingIdR : {auto__con : RingWithUnityty} -> (r : ty) ->unity<.>r=r
Visibility: public export
interfaceField : Type->Type
  Sets equipped with two binary operations – both associative,
commutative and possessing a neutral element – and distributivity
laws relating the two operations. All elements except the additive
identity should have a multiplicative inverse. Should (but may
not) satisfy the following laws:

+ Associativity of `<+>`:
forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+ Commutativity of `<+>`:
forall a b, a <+> b == b <+> a
+ Neutral for `<+>`:
forall a, a <+> neutral == a
forall a, neutral <+> a == a
+ Inverse for `<+>`:
forall a, a <+> inverse a == neutral
forall a, inverse a <+> a == neutral
+ Associativity of `<.>`:
forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
+ Unity for `<.>`:
forall a, a <.> unity == a
forall a, unity <.> a == a
+ InverseM of `<.>`, except for neutral
forall a /= neutral, a <.> inverseM a == unity
forall a /= neutral, inverseM a <.> a == unity
+ Distributivity of `<.>` and `<+>`:
forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

Parameters: ty
Constraints: RingWithUnity ty
Methods:
inverseM : (x : ty) ->Not (x=neutral) ->ty
inverseM : {auto__con : Fieldty} -> (x : ty) ->Not (x=neutral) ->ty
Visibility: public export