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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.SizedTypes.Utils

Synopsis

- debug :: IORef Bool
- setDebugging :: Bool -> IO ()
- trace :: String -> a -> a
- traceM :: Applicative f => String -> f ()
- class Eq a => Top a where
  - top :: a
  - isTop :: a -> Bool
- class Plus a b c where
  - plus :: a -> b -> c
- class MeetSemiLattice a where
  - meet :: a -> a -> a
- class (MeetSemiLattice a, Top a) => Dioid a where
  - compose :: a -> a -> a
  - unitCompose :: a

# Documentation

debug :: IORef Bool Source #

setDebugging :: Bool -> IO () Source #

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 Methods top :: Label Source # isTop :: Label -> Bool Source #
Top Weight Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods top :: Weight Source # isTop :: Weight -> Bool Source #
(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.Syntax Methods plus :: NamedRigid -> Int -> NamedRigid Source #
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 Methods compose :: Cmp -> Cmp -> Cmp Source # unitCompose :: Cmp Source #
Dioid Label Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods compose :: Label -> Label -> Label Source # unitCompose :: Label Source #
Dioid Weight Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.WarshallSolver Methods compose :: Weight -> Weight -> Weight Source # unitCompose :: Weight Source #
(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 #