Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.With
Synopsis
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
= Here
| ArgPat Int ConPos
updateWithConstructorRanges :: [Telescope] -> [Arg Pattern] -> RHS -> [Arg Pattern]
constructorsInClauses :: ConPos -> [Clause] -> [Range]
constructorsInClause :: ConPos -> Clause -> [Range]
Documentation
withFunctionType :: Telescope -> [Term] -> [Type] -> Telescope -> Type -> TCM TypeSource
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
patsToTerms :: [Arg Pattern] -> [Arg Term]Source
data ConPos Source
Constructors
Here
ArgPat Int ConPos
updateWithConstructorRanges :: [Telescope] -> [Arg Pattern] -> RHS -> [Arg Pattern]Source
constructorsInClauses :: ConPos -> [Clause] -> [Range]Source
constructorsInClause :: ConPos -> Clause -> [Range]Source
Produced by Haddock version 2.6.0