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