Agda.TypeChecking.SizedTypes.Utils

Documentation

debug :: Bool

trace :: String -> a -> a

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

($>) :: Functor f => f b -> a -> f a

class Eq a => Top a where

Methods

top :: a

isTop :: a -> Bool

Instances

Top Cmp

Top Label

Top Weight

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

class Plus a b c where

Methods

plus :: a -> b -> c

Instances

Plus Int Int Int

Plus Offset Weight Weight

Plus Weight Offset Weight

Plus NamedRigid Int NamedRigid

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

Add offset to size expression.

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

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

class MeetSemiLattice a where

Methods

meet :: a -> a -> a

Instances

MeetSemiLattice Cmp

MeetSemiLattice Offset

MeetSemiLattice Label

MeetSemiLattice Weight

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

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

Semiring with idempotent + == dioid

Methods

compose

Arguments

:: a

-> a

-> a

E.g. +

unitCompose

Arguments

:: a

neutral element of compose, e.g. zero

Instances

Dioid Cmp

Dioid Label

Dioid Weight

(Show r, Show f, Show a, Ord r, Ord f, Dioid a) => Dioid (Edge' r f a)