Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.x8174fa42026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 8174fa4 · 2026-10-11

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Coverage.Cubical

6 values

PackageAgda-2.8.0.2
Exports6
LanguageHaskell2010
LicenceMIT
SourceCubical.hs

valuecreateMissingIndexedClauses

:: QName
-> Arg Nat
-> BlockingVar
-> SplitClause
-> [(SplitTag, (SplitClause, IInfo))]
-> [Clause]
-> TCM ([(SplitTag, CoverResult)], [Clause])

valuecovFillTele :: QName -> Abs Telescope -> Term -> Args -> Term -> TCM [Term]

valuecreateMissingTrXTrXClause

:: QName
trX
-> QName
f defined
-> Arg Nat
-> BlockingVar
-> SplitClause
-> TCM Clause

valuecreateMissingTrXHCompClause

:: QName
-> QName
-> Arg Nat
-> BlockingVar
-> SplitClause
-> TCM Clause

valuecreateMissingTrXConClause

:: QName
-> QName
-> Arg Nat
-> BlockingVar
-> SplitClause
-> QName
-> UnifyEquiv
-> TCM Clause

valuecreateMissingHCompClause

:: 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.