| 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.4.2