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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.SizedTypes.Utils

Synopsis

Documentation

trace :: String -> a -> a Source

class Eq a => Top a where Source

Minimal complete definition

top

Methods

top :: a Source

isTop :: a -> Bool Source

Instances

class (MeetSemiLattice a, Top a) => Dioid a where Source

Semiring with idempotent + == dioid

Methods

compose Source

Arguments

:: a 
-> a 
-> a

E.g. +

unitCompose Source

Arguments

:: a

neutral element of compose, e.g. zero

Instances