- withFunctionType :: Telescope -> [Term] -> [Type] -> Telescope -> Type -> TCM Type
- buildWithFunction :: QName -> Telescope -> [Arg Pattern] -> Permutation -> Nat -> Nat -> [Clause] -> TCM [Clause]
- stripWithClausePatterns :: Telescope -> [Arg Pattern] -> Permutation -> [NamedArg Pattern] -> TCM [NamedArg Pattern]
- withDisplayForm :: QName -> QName -> Telescope -> Telescope -> Nat -> [Arg Pattern] -> Permutation -> TCM DisplayForm
- patsToTerms :: [Arg Pattern] -> [Arg Term]
- data ConPos
- updateWithConstructorRanges :: [Telescope] -> [Arg Pattern] -> RHS -> [Arg Pattern]
- constructorsInClauses :: ConPos -> [Clause] -> [Range]
- constructorsInClause :: ConPos -> Clause -> [Range]
Documentation
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
constructorsInClauses :: ConPos -> [Clause] -> [Range]Source
constructorsInClause :: ConPos -> Clause -> [Range]Source