- 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

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 DisplayTerm]Source