| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
The option is still there, but not documented since it is too
dangerous. Hints and type classes instances are not taking cleared
variables into account.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Marking it as experimental.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
global environment (we use throughout the document)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
needed
|
|
shown in the previous example
|
|
|
|
We have expanded the example above.
For consistency reasons, it would make sense to do the same also for this example.
However, due to the size of the terms, it is hard to typeset it nicely.
I propose to remove it.
|
|
|
|
|
|
definition'? Doesn't make more sense to refer to it as 'inductive type'?
|
|
definition.
|
|
|
|
|
|
|
|
|
|
|
|
|
