Agda.TypeChecking.Coverage.Cubical

Documentation

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

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

createMissingTrXTrXClause

Arguments

:: QName

trX

-> QName

f defined

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

Arguments

:: QName

function being defined

-> Arg Nat

covSplitArg index

-> BlockingVar

x variable being split on.

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

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.