Chapter4

[ghost]

I've incorporated your feedback from yesterday.

[ghost]

These commits we haven't reviewed together yet:

• 456148d 2015-11-12 | TYPOGRAPHY: adjustments (HEAD, chapter4)

  Various little changes.

  • removing unnecessary paragraph indentation
  • some single-sentence paragraphs were merged with the previous paragraphs

• dc7e0e2 2015-11-10 | PROPOSITION: the side-condition was made more specific.

• c4af151 2015-11-10 | PROPOSITION: rephrasing of the explanation of the meaning of '[I:A|B]'

• c26afd8 2015-11-10 | PROPOSITION: Added an explicit definition of the notation for enriching the global environment (we use throughout the document)

• f4fc000 2015-11-09 | PROPOSITION: Added "if" and "then" words missing in the original sentence.

• a40b908 2015-11-09 | PROPOSITION: Example was simplified

• ce6b80d 2015-11-05 | FIX: removing references to Γ which is not defined in a given context

• 988e217 2015-11-05 | CLEANUP PROPOSITION: superfluous parentheses were removed

• 42eca93 2015-11-05 | CLEANUP PROPOSITION: s/local context of parameters/context of parameters

• 0c10882 2015-11-05 | CLEANUP PROPOSITION: removed unnecessary sentence.

• 80b09a9 2015-11-04 | FIX: removing a reference to \Gamma, because it is undefined

• a86b67b 2015-11-04 | CLEANUP PROPOSITION: s/Γ_P; Γ_C/Γ_P ∪ Γ_C/

• b751382 2015-11-04 | ALPHA-CONVERSION: to some simpler names

• 1140997 2015-11-03 | ENH: examples for 'strict positivity' were expanded

• c6bd639 2015-11-03 | CLEANUP: s/List_A/List~A/g

• 6df95ad 2015-11-03 | CLEANUP: the definition of "type of constructor" was rephrased in order to make it more clear

• 9d035a2 2015-11-02 | ENH: adding a definition of the concept "_ is an arity".

• 0def0ab 2015-11-02 | CLEANUP: Presentation of examples was changed to make them more comprehensible.

[herbelin]

Hi, all these extra commits we did not already reviewed look good to me, up to the following exceptions.

• In a86b67b, it should really be concatenation of lists, hence ";", and not union, as if there were sets. But maybe, what is missing is a sentence somewhere to explain that ";" is concatenation.
• Also, in b751382, I'm sensitive to your motivation to simplify names, but since "t" is already used for terms, we would have to find another letter than s for sorts. Maybe r, if you insist in preferring r to s', and then we shall say somewhere that both r and s are used to denote sorts.
• In 6df95ad, I would prefer that we say "that T is", or "that the expression T is", rather than 'that the term T is", because T is a type and it might be confusing to call it a term while it is more precisely a type. Also in the clauses, I would prefer we say "$T$ is $(I~t_1\ldots ~t_n)$ and similarly on the next line, so that there is no confusion with the symbol = which already has a meaning as a Coq term. Otherwise said, "is" is the equal sign of the metalanguage, the same way as "for all" is the ∀ sign of the metalanguage.

I also slightly hesitated about 0c10882, but after all, I agree that this information is more difficult to understand than useful.

[ghost]

Makes sense.

Commit a86b67b was reverted
and commit eed6e8c now replaces it.

Commit b751382 was reverted.

Commit 6df95ad was reverted
and commit a810f3b now replaces it.

Commit 0c10882 was reverted.

[ghost]

As you suggested on Friday evening, commit b0b0da6 changes the way how examples:

1. of formal representation inductive definitions
2. of proofs of strictly positive occurrence
   are presented.

These examples are now presented as (framed) figures which interested reader may inspect and uninterested reader can easily skip.

The figures are kept close to the position where their contents is relevant.