Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Termination.Semiring

Description

Semirings.

Synopsis

- class Eq a => HasZero a where
  - zeroElement :: a
- data Semiring a = Semiring {
  - add :: a -> a -> a
  - mul :: a -> a -> a
  - zero :: a
  }
- integerSemiring :: Semiring Integer
- intSemiring :: Semiring Int
- boolSemiring :: Semiring Bool

# Documentation

class Eq a => HasZero a where Source #

`HasZero` is needed for sparse matrices, to tell which is the element that does not have to be stored. It is a cut-down version of `SemiRing` which is definable without the implicit `?cutoff`.

Methods

zeroElement :: a Source #

#### Instances

Instances details

HasZero Order Source # |
Instance details Defined in Agda.Termination.Order Methods zeroElement :: Order Source #
HasZero Integer Source # | The standard semiring on `Integer`s.
Instance details Defined in Agda.Termination.Semiring Methods zeroElement :: Integer Source #
HasZero Int Source # | The standard semiring on `Int`s.
Instance details Defined in Agda.Termination.Semiring Methods zeroElement :: Int Source #

data Semiring a Source #

Semirings.

Constructors

Semiring |

Fields

- add :: a -> a -> a

  Addition.

- mul :: a -> a -> a

  Multiplication.

- zero :: a

  Zero. The one is never used in matrix multiplication , one :: a -- ^ One.

integerSemiring :: Semiring Integer Source #

intSemiring :: Semiring Int Source #

boolSemiring :: Semiring Bool Source #

The standard semiring on `Bool`s.