Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Termination.Semiring

Description

Semirings.

Synopsis

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

HasZero Integer Source #

The standard semiring on Integers.

Instance details

Defined in Agda.Termination.Semiring

Methods

zeroElement :: Integer Source #

HasZero Int Source #

The standard semiring on Ints.

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.

boolSemiring :: Semiring Bool Source #

The standard semiring on Bools.