Safe Haskell | None |
---|---|
Language | Haskell98 |
- withFunctionType :: Telescope -> [Term] -> [Type] -> Telescope -> Type -> TCM Type
- buildWithFunction :: QName -> Telescope -> [NamedArg Pattern] -> Permutation -> Nat -> Nat -> [SpineClause] -> TCM [SpineClause]
- stripWithClausePatterns :: Telescope -> [NamedArg Pattern] -> Permutation -> [NamedArg Pattern] -> TCM [NamedArg Pattern]
- withDisplayForm :: QName -> QName -> Telescope -> Telescope -> Nat -> [NamedArg Pattern] -> Permutation -> Permutation -> TCM DisplayForm
- patsToTerms :: Permutation -> [NamedArg Pattern] -> [Arg DisplayTerm]
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 = 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 Δ
)
:: QName | The name of parent function. |
-> QName | The name of the with-function. |
-> Telescope | The arguments of the with function before the with exprs. |
-> Telescope | The arguments of the with function after the with exprs. |
-> Nat | The number of with expressions. |
-> [NamedArg Pattern] | The parent patterns. |
-> Permutation | Permutation to split into needed and unneeded vars. |
-> Permutation | Permutation reordering the variables in parent patterns. |
-> TCM DisplayForm |
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.
patsToTerms :: Permutation -> [NamedArg Pattern] -> [Arg DisplayTerm] Source