ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.Coverage.Cubical
- 7 values
- PackageAgda-2.7.0.1
- Exports7
- LanguageHaskell2010
- LicenceMIT
- SourceCubical.hs
value
createMissingTrXTrXClause :: QNametrX
-> QNamef defined
-> Arg Nat-> BlockingVar-> SplitClause-> TCM Clause
If given TheInfo{} then assumes "x : Id u v" and
returns both a SplittingDone for conId, and the Clause that covers it.
value
createMissingHCompClause :: QNameFunction name.
-> Arg Natindex of hcomp pattern
-> BlockingVarBlocking var that lead to hcomp split.
-> SplitClauseClause before the hcomp split
-> SplitClauseClause to add.
-> [Clause]-> TCM ([(SplitTag, CoverResult)], [Clause])
Append an hcomp clause to the clauses of a function.