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




buildWithFunction :: QName -> Telescope -> [Arg Pattern] -> Permutation -> Nat -> Nat -> [Clause] -> TCM [Clause]Source

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

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

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