| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
elimination sorts" is actually used
|
|
|
|
|
