Closed andrejbauer closed 4 years ago
If a primitive rule R is used in a non-applied form, then it is automatically converted to a derivation. For example:
R
# rule Pi (A type) ({_ : A} _ type) type Rule Pi is postulated. # Pi - : derivation = derive (A type) ({_ : A} _ type) → Pi A ({x₀} _ {x₀}) type
Previously, typing Pi like that would just give an error (saying that Pi must be applied exactly once).
Pi
If a primitive rule
Ris used in a non-applied form, then it is automatically converted to a derivation. For example:Previously, typing
Pilike that would just give an error (saying thatPimust be applied exactly once).