diff options
| -rw-r--r-- | doc/sphinx/language/cic.rst | 56 |
1 files changed, 22 insertions, 34 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 5a2aa0a1f..f6bab0267 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -917,45 +917,33 @@ condition* for a constant :math:`X` in the following cases: satisfies the nested positivity condition for :math:`X` -For instance, if one considers the type - .. example:: - .. coqtop:: all + For instance, if one considers the following variant of a tree type + branching over the natural numbers: + + .. coqtop:: in - Module TreeExample. - Inductive tree (A:Type) : Type := - | leaf : tree A - | node : A -> (nat -> tree A) -> tree A. + 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``: - [TODO Note: This commentary does not seem to correspond to the - preceding example. Instead it is referring to the first example - in Inductive Definitions section. It seems we should either - delete the preceding example and refer the the example above of - type `list A`, or else we should rewrite the commentary below.] - - Then every instantiated constructor of list A satisfies the nested positivity - condition for list - │ - ├─ concerning type list A of constructor nil: - │ Type list A of constructor nil satisfies the positivity condition for list - │ because list does not appear in any (real) arguments of the type of that - | constructor (primarily because list does not have any (real) - | arguments) ... (bullet 1) - │ - ╰─ concerning type ∀ A → list A → list A of constructor cons: - Type ∀ A : Type, A → list A → list A of constructor cons - satisfies the positivity condition for list because: - │ - ├─ list occurs only strictly positively in Type ... (bullet 3) - │ - ├─ list occurs only strictly positively in A ... (bullet 3) - │ - ├─ list occurs only strictly positively in list A ... (bullet 4) - │ - ╰─ list satisfies the positivity condition for list A ... (bullet 1) + + Type ``nattree A`` of constructor ``leaf`` satisfies the positivity condition for + ``nattree`` because ``nattree`` does not appear in any (real) arguments of the + type of that constructor (primarily because ``nattree`` does not have any (real) + arguments) ... (bullet 1) + + + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the + positivity condition for ``nattree`` because: + + - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 3) + + - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2) + + - ``nattree`` satisfies the positivity condition for ``nattree A`` ... (bullet 1) .. _Correctness-rules: |