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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.SizedTypes.Utils

Synopsis

Documentation

trace :: String -> a -> a

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

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

class Eq a => Top a where

Minimal complete definition

top

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

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)