| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Coverage.Cubical
Synopsis
- createMissingIndexedClauses :: QName -> Arg Nat -> BlockingVar -> SplitClause -> [(SplitTag, (SplitClause, IInfo))] -> [Clause] -> TCM ([(SplitTag, CoverResult)], [Clause])
- covFillTele :: QName -> Abs Telescope -> Term -> Args -> Term -> TCM [Term]
- createMissingTrXTrXClause :: QName -> QName -> Arg Nat -> BlockingVar -> SplitClause -> TCM Clause
- createMissingTrXHCompClause :: QName -> QName -> Arg Nat -> BlockingVar -> SplitClause -> TCM Clause
- createMissingTrXConClause :: QName -> QName -> Arg Nat -> BlockingVar -> SplitClause -> QName -> UnifyEquiv -> TCM Clause
- createMissingHCompClause :: QName -> Arg Nat -> BlockingVar -> SplitClause -> SplitClause -> [Clause] -> TCM ([(SplitTag, CoverResult)], [Clause])
Documentation
createMissingIndexedClauses :: QName -> Arg Nat -> BlockingVar -> SplitClause -> [(SplitTag, (SplitClause, IInfo))] -> [Clause] -> TCM ([(SplitTag, CoverResult)], [Clause]) Source #
createMissingTrXTrXClause Source #
Arguments
| :: QName | trX |
| -> QName | f defined |
| -> Arg Nat | |
| -> BlockingVar | |
| -> SplitClause | |
| -> TCM Clause |
createMissingTrXHCompClause :: QName -> QName -> Arg Nat -> BlockingVar -> SplitClause -> TCM Clause Source #
createMissingTrXConClause :: QName -> QName -> Arg Nat -> BlockingVar -> SplitClause -> QName -> UnifyEquiv -> TCM Clause Source #
createMissingHCompClause Source #
Arguments
| :: QName | Function name. |
| -> Arg Nat | index of hcomp pattern |
| -> BlockingVar | Blocking var that lead to hcomp split. |
| -> SplitClause | Clause before the hcomp split |
| -> SplitClause | Clause to add. |
| -> [Clause] | |
| -> TCM ([(SplitTag, CoverResult)], [Clause]) |
Append an hcomp clause to the clauses of a function.