Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Coverage.SplitClause
Description
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 #
Constructors
SClause | |
Fields
|
Instances
PrettyTCM SplitClause Source # | For debugging only. |
Defined in Agda.TypeChecking.Coverage Methods prettyTCM :: MonadPretty m => SplitClause -> m Doc Source # |
data UnifyEquiv Source #
Constructors
UE | |
Fields
|
Instances
Show UnifyEquiv Source # | |
Defined in Agda.TypeChecking.Coverage.SplitClause Methods showsPrec :: Int -> UnifyEquiv -> ShowS show :: UnifyEquiv -> String showList :: [UnifyEquiv] -> ShowS |
Constructors
TheInfo UnifyEquiv | |
NoInfo |
A Covering
is the result of splitting a SplitClause
.
Constructors
Covering | |
Fields
|
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 #
Constructors
CoverResult | |
Fields
|