| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Positivity
Contents
Description
Check that a datatype is strictly positive.
Synopsis
- checkStrictlyPositive :: MutualInfo -> Set QName -> TCM ()
- getDefArity :: Definition -> TCM Int
- hasDefinition :: Defn -> Bool
- isDatatype :: Definition -> Maybe (PositivityCheck, DataOrRecord)
- preprocessBlock :: [QName] -> TCM (Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)])
Documentation
checkStrictlyPositive :: MutualInfo -> Set QName -> TCM () Source #
Check that the datatypes in the mutual block containing the given declarations are strictly positive.
Find polarity of datatypes parameters and indices.
Also add information about positivity and recursivity of records to the signature.
getDefArity :: Definition -> TCM Int Source #
hasDefinition :: Defn -> Bool Source #
isDatatype :: Definition -> Maybe (PositivityCheck, DataOrRecord) Source #
preprocessBlock :: [QName] -> TCM (Maybe [(QName, Int, Maybe (PositivityCheck, DataOrRecord), Bool)]) Source #
Orphan instances
| PrettyTCM Node Source # | |
| PrettyTCM (Seq OccursWhere) Source # | |
Methods prettyTCM :: MonadPretty m => Seq OccursWhere -> m Doc Source # | |
| Pretty a => PrettyTCMWithNode (Edge a) Source # | |
Methods prettyTCMWithNode :: (PrettyTCM n, MonadPretty m) => WithNode n (Edge a) -> m Doc Source # | |