Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Coverage.Cubical

Synopsis

Documentation

createMissingConIdClause Source #

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