| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
I also renamed the type to nattree (see discussion on
https://github.com/coq/coq/pull/5979) to disambiguate from another,
earlier example.
|
|
|
|
|
|
Work done by Assia Mahboubi and Enrico Tassi
|
|
|
|
|
|
|
|
|
|
Since About mentions it the doc should as well.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
