Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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

Instances details
Top Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

top :: Cmp Source #

isTop :: Cmp -> Bool Source #

Top Label Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Top Weight Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

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

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

top :: Edge' r f a Source #

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

class Plus a b c where Source #

Methods

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

Instances

Instances details
Plus NamedRigid Int NamedRigid Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Plus Offset Offset Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

plus :: Offset -> Offset -> Offset Source #

Plus Offset Weight Weight Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: Offset -> Weight -> Weight Source #

Plus Weight Offset Weight Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: Weight -> Offset -> Weight Source #

Plus Int Int Int Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Utils

Methods

plus :: Int -> Int -> Int Source #

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

Add offset to size expression.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

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

Plus (SizeExpr' r f) Label (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

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

Plus (SizeExpr' r f) Weight (SizeExpr' r f) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

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

class MeetSemiLattice a where Source #

Methods

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

Instances

Instances details
MeetSemiLattice Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

meet :: Cmp -> Cmp -> Cmp Source #

MeetSemiLattice Offset Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Methods

meet :: Offset -> Offset -> Offset Source #

MeetSemiLattice Label Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

meet :: Label -> Label -> Label Source #

MeetSemiLattice Weight Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

meet :: Weight -> Weight -> Weight Source #

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

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

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

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

Instances details
Dioid Cmp Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Syntax

Dioid Label Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Dioid Weight Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

(Ord r, Ord f, Dioid a) => Dioid (Edge' r f a) Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

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

unitCompose :: Edge' r f a Source #