Agda-2.2.6: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.Termination.Semiring
Description
Semirings.
Synopsis
data
Semiring
a =
Semiring
{
add
:: a -> a -> a
mul
:: a -> a -> a
zero
:: a
one
:: a
}
semiringInvariant
:: (
Arbitrary
a,
Eq
a,
Show
a) =>
Semiring
a -> a -> a -> a ->
Bool
integerSemiring
::
Semiring
Integer
boolSemiring
::
Semiring
Bool
tests
::
IO
Bool
Documentation
data
Semiring
a
Source
Semirings.
Constructors
Semiring
add
:: a -> a -> a
Addition.
mul
:: a -> a -> a
Multiplication.
zero
:: a
Zero.
one
:: a
One.
semiringInvariant
:: (
Arbitrary
a,
Eq
a,
Show
a) =>
Semiring
a -> a -> a -> a ->
Bool
Source
Semiring invariant.
integerSemiring
::
Semiring
Integer
Source
The standard semiring on
Integer
s.
boolSemiring
::
Semiring
Bool
Source
The standard semiring on
Bool
s.
tests
::
IO
Bool
Source
Produced by
Haddock
version 2.6.0