|
Agda.TypeChecking.Substitute |
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
Apply something to a bunch of arguments.
Preserves blocking tags (application can never resolve blocking).
| | Methods | | | Instances | |
|
|
|
The type must contain the right number of pis without have to perform any
reduction.
|
|
|
(abstract args v) args --> v[args].
| | Methods | | | Instances | |
|
|
|
|
|
Substitute a term for the nth free variable.
| | Methods | | | Instances | |
|
|
|
|
|
|
|
Instantiate an abstraction
|
|
|
Add k to index of each open variable in x.
| | Methods | | | Instances | |
|
|
|
|
|
|
|
|
|
|
|
|
Everything will be a pi.
|
|
|
|
Produced by Haddock version 2.4.2 |