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 = p'

- 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 :: QName -> QName -> Telescope -> Telescope -> Nat -> [NamedArg Pattern] -> Permutation -> Permutation -> 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]