IdrisDoc
: Interfaces.Verified
Index
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