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 #

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

class Eq a => Top a where #

Minimal complete definition

top

Methods

top :: a #

isTop :: a -> Bool #

Instances

Top Cmp # 

Methods

top :: Cmp #

isTop :: Cmp -> Bool #

Top Label # 

Methods

top :: Label #

isTop :: Label -> Bool #

Top Weight # 

Methods

top :: Weight #

isTop :: Weight -> Bool #

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

Methods

top :: Edge' r f a #

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

class Plus a b c where #

Minimal complete definition

plus

Methods

plus :: a -> b -> c #

Instances

Plus Int Int Int # 

Methods

plus :: Int -> Int -> Int #

Plus Offset Offset Offset # 

Methods

plus :: Offset -> Offset -> Offset #

Plus Offset Weight Weight # 

Methods

plus :: Offset -> Weight -> Weight #

Plus Weight Offset Weight # 

Methods

plus :: Weight -> Offset -> Weight #

Plus NamedRigid Int NamedRigid # 

Methods

plus :: NamedRigid -> Int -> NamedRigid #

Plus (SizeExpr' r f) Offset (SizeExpr' r f) #

Add offset to size expression.

Methods

plus :: SizeExpr' r f -> Offset -> SizeExpr' r f #

Plus (SizeExpr' r f) Label (SizeExpr' r f) # 

Methods

plus :: SizeExpr' r f -> Label -> SizeExpr' r f #

Plus (SizeExpr' r f) Weight (SizeExpr' r f) # 

Methods

plus :: SizeExpr' r f -> Weight -> SizeExpr' r f #

class MeetSemiLattice a where #

Minimal complete definition

meet

Methods

meet :: a -> a -> a #

Instances

MeetSemiLattice Cmp # 

Methods

meet :: Cmp -> Cmp -> Cmp #

MeetSemiLattice Offset # 

Methods

meet :: Offset -> Offset -> Offset #

MeetSemiLattice Label # 

Methods

meet :: Label -> Label -> Label #

MeetSemiLattice Weight # 

Methods

meet :: Weight -> Weight -> Weight #

(Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a) # 

Methods

meet :: Edge' r f a -> Edge' r f a -> Edge' r f a #

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

Semiring with idempotent + == dioid

Minimal complete definition

compose, unitCompose

Methods

compose :: a -> a -> a #

unitCompose :: a #

Instances

Dioid Cmp # 

Methods

compose :: Cmp -> Cmp -> Cmp #

unitCompose :: Cmp #

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

Methods

compose :: Edge' r f a -> Edge' r f a -> Edge' r f a #

unitCompose :: Edge' r f a #