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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.SizedTypes.Utils

Synopsis

Documentation

trace :: String -> a -> a Source #

traceM :: Applicative f => String -> f () Source #

class Eq a => Top a where Source #

Minimal complete definition

top

Methods

top :: a Source #

isTop :: a -> Bool Source #

Instances

Top Cmp Source # 

Methods

top :: Cmp Source #

isTop :: Cmp -> Bool Source #

Top Label Source # 
Top Weight Source # 
(Ord r, Ord f, Top a) => Top (Edge' r f a) Source # 

Methods

top :: Edge' r f a Source #

isTop :: Edge' r f a -> Bool Source #

class Plus a b c where Source #

Minimal complete definition

plus

Methods

plus :: a -> b -> c Source #

Instances

class MeetSemiLattice a where Source #

Minimal complete definition

meet

Methods

meet :: a -> a -> a Source #

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

Semiring with idempotent + == dioid

Minimal complete definition

compose, unitCompose

Methods

compose :: a -> a -> a Source #

unitCompose :: a Source #

Instances