Agda.TypeChecking.With

Documentation

withFunctionType :: Telescope -> [Term] -> [Type] -> Telescope -> Type -> TCM Type

buildWithFunction :: QName -> Telescope -> [NamedArg Pattern] -> Permutation -> Nat -> Nat -> [SpineClause] -> TCM [SpineClause]

Compute the clauses for the with-function given the original patterns.

stripWithClausePatterns :: Telescope -> [NamedArg Pattern] -> Permutation -> [NamedArg Pattern] -> TCM [NamedArg Pattern]

stripWithClausePatterns Γ qs π ps = ps'

Δ - context bound by lhs of original function (not an argument)

Γ - type of arguments to original function

qs - internal patterns for original function

π - permutation taking vars(qs) to support(Δ)

ps - patterns in with clause (presumably of type Γ)

ps' - patterns for with function (presumably of type Δ)

withDisplayForm

Arguments

:: QName

The name of parent function.

-> QName

The name of the with-function.

-> Telescope

The arguments of the with function before the with exprs.

-> Telescope

The arguments of the with function after the with exprs.

-> Nat

The number of with expressions.

-> [NamedArg Pattern]

The parent patterns.

-> Permutation

Permutation to split into needed and unneeded vars.

-> Permutation

Permutation reordering the variables in parent patterns.

-> TCM DisplayForm

Construct the display form for a with function. It will display applications of the with function as applications to the original function. For instance, aux a b c as f (suc a) (suc b) | c

n is the number of with arguments.

patsToTerms :: Permutation -> [NamedArg Pattern] -> [Arg DisplayTerm]