| 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
- createMissingConIdClause :: QName -> Arg Nat -> BlockingVar -> SplitClause -> IInfo -> TCM (Maybe ((SplitTag, SplitTree), 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 #
createMissingConIdClause Source #
Arguments
| :: QName | function being defined |
| -> Arg Nat |
|
| -> BlockingVar |
|
| -> SplitClause | clause before split |
| -> IInfo | info from unification |
| -> TCM (Maybe ((SplitTag, SplitTree), Clause)) |
If given TheInfo{} then assumes "x : Id u v" and
returns both a SplittingDone for conId, and the Clause that covers it.
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.