Safe Haskell | None |
---|---|
Language | Haskell2010 |
SplitClause and CoverResult types.
Synopsis
- data SplitClause = SClause {
- scTel :: Telescope
- scPats :: [NamedArg SplitPattern]
- scSubst :: Substitution' SplitPattern
- scCheckpoints :: Map CheckpointId Substitution
- scTarget :: Maybe (Dom Type)
- data UnifyEquiv = UE {}
- data IInfo
- data Covering = Covering {
- covSplitArg :: Arg Nat
- covSplitClauses :: [(SplitTag, (SplitClause, IInfo))]
- splitClauses :: Covering -> [SplitClause]
- clauseToSplitClause :: Clause -> SplitClause
- data CoverResult = CoverResult {
- coverSplitTree :: SplitTree
- coverUsedClauses :: IntSet
- coverMissingClauses :: [(Telescope, [NamedArg DeBruijnPattern])]
- coverPatterns :: [Clause]
- coverNoExactClauses :: IntSet
Documentation
data SplitClause Source #
SClause | |
|
Instances
PrettyTCM SplitClause Source # | For debugging only. |
Defined in Agda.TypeChecking.Coverage prettyTCM :: MonadPretty m => SplitClause -> m Doc Source # |
data UnifyEquiv Source #
UE | |
|
Instances
Show UnifyEquiv Source # | |
Defined in Agda.TypeChecking.Coverage.SplitClause showsPrec :: Int -> UnifyEquiv -> ShowS show :: UnifyEquiv -> String showList :: [UnifyEquiv] -> ShowS |
A Covering
is the result of splitting a SplitClause
.
Covering | |
|
splitClauses :: Covering -> [SplitClause] Source #
Project the split clauses out of a covering.
clauseToSplitClause :: Clause -> SplitClause Source #
Create a split clause from a clause in internal syntax. Used by make-case.
data CoverResult Source #
CoverResult | |
|