Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 #

covFillTele :: QName -> Abs Telescope -> Term -> Args -> Term -> TCM [Term] 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.