diff options
| author | Tanaka Akira | 2019-01-31 15:54:57 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 15:54:57 +0900 |
| commit | b090f65cf35e45596c10a7513bb3e8058069e4fd (patch) | |
| tree | 13b1a033a6e08c30994c9c77abf03b0ac5a5450b /doc/sphinx | |
| parent | 81c6a88eb261c9e130aff73f2d5bc1ee1f7e0758 (diff) | |
Remove "End TreeExample." line.
This corresponds to "Module TreeExample." removed at
2018-04-24 bcf5352cc7a26a672e719f7dad4021c69d723833.
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 25a230015c..6ddfe14eea 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -930,7 +930,6 @@ condition* for a constant :math:`X` in the following cases: Inductive nattree (A:Type) : Type := | leaf : nattree A | node : A -> (nat -> nattree A) -> nattree A. - End TreeExample. Then every instantiated constructor of ``nattree A`` satisfies the nested positivity condition for ``nattree``: |