| 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
- 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
setDebugging :: Bool -> IO () Source #
traceM :: Applicative f => String -> f () Source #
class Eq a => Top a where Source #
Minimal complete definition
class Plus a b c where Source #
Instances
| Plus Int Int Int Source # | |
| Plus Offset Offset Offset Source # | |
| Plus Offset Weight Weight Source # | |
| Plus Weight Offset Weight Source # | |
| Plus NamedRigid Int NamedRigid Source # | |
Defined in Agda.TypeChecking.SizedTypes.Solve Methods plus :: NamedRigid -> Int -> NamedRigid Source # | |
| Plus (SizeExpr' r f) Offset (SizeExpr' r f) Source # | Add offset to size expression. |
| Plus (SizeExpr' r f) Label (SizeExpr' r f) Source # | |
| Plus (SizeExpr' r f) Weight (SizeExpr' r f) Source # | |
class MeetSemiLattice a where Source #
Instances
| MeetSemiLattice Cmp Source # | |
| MeetSemiLattice Offset Source # | |
| MeetSemiLattice Label Source # | |
| MeetSemiLattice Weight Source # | |
| (Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a) Source # | |
class (MeetSemiLattice a, Top a) => Dioid a where Source #
Semiring with idempotent + == dioid
Methods
Arguments
| :: a | |
| -> a | |
| -> a | E.g. + |
Arguments
| :: a | neutral element of |