Agda-2.4.0: A dependently typed functional programming language and proof assistant

Safe HaskellNone

Agda.TypeChecking.With

Synopsis

Documentation

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

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

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

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 DisplayFormSource

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.