| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 Type | Source

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 DisplayForm | Source

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.4.2