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

Safe Haskell | None

Agda.TypeChecking.With

Synopsis

- showPat :: Pattern -> TCM Doc
- 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 DisplayTerm]

# Documentation

showPat :: Pattern -> TCM Doc

withFunctionType :: Telescope -> [Term] -> [Type] -> Telescope -> Type -> TCM Type

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

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

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

    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

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 :: [Arg Pattern] -> [Arg DisplayTerm]