Fix small errors in cic.rst.

Fix small errors in cic.rst:

* 3.4.1 Free variables: use :math: for "∀ x:T,~U".
  :g: doesn't show "∀" in PDF.
  "λx:T.~U" is also changed to :math: to use consistent font.
* 3.4.3 Zeta: ":U" added in "let x:=u:U in t" to be valid let-in expression.
* 3.4.3 convertibility: add :math: for u_2' to apply math formatting.
* 3.4.4.6: fix index. "n" should be "k" because they corresponds k-th
  constructor.
* 3.4.5 Type constructor: I changed the section title "Type constructor" to
  "Type of constructor".
  "Type constructor" means a feature to construct new type.
  But this section describes about a type of constructor.
* 3.4.5 Example nattree: The reason of
  "``nattree`` occurs only strictly positively in ``A``" should be
  bullet 1 instead of bullet 3.
  The bullet 3 of strict positivity definition is about product, "∀x ∶ U , V",
  but "A" is not a product.
* 3.4.5 Destructors: use :math: for "∀".
  :g: doesn't show "∀" in PDF.
  Also, :math: is used for expressions which has no "∀" character
  for font consistency.
  Note that I use \kw{has}\_\kw{length} instead of
  \kw{has\_length} because the latter is formatted as has\_length in HTML.
  (the backslash is retained.)
* 3.4.5 list example: curly braces added.
* 3.4.5 Fixpoint definition: add :math: for Γ_i to apply math formatting.
* 3.4.6 2nd rule of First abstracting property: use \subst.
  This adds a curly brace.

Also, spacing and fonts are adjusted as follows.

* 3.4.1 let-in term: use :math: for variable x, consistent with other term
  descriptions.
* 3.4.1 let-in term: use \letin command for concrete let-in term.
* 3.4.2 Note: insert spaces as ((λ x:T.~u)~t).
  Since T is more closely reated to x than u, T should be positioned
  close to x than u.
  Since it seems most application has a space, I inserted a space here
  for consistency.
* 3.4.3 beta-reduction: insert spaces as 3.4.2.
* 3.4.3 eta-expansion: insert spaces as 3.4.2.
* 3.4.5 Example: use sans-serif fonts for constructor "O" and "S".
* 3.4.5 Fixpoint definition: insert spaces around "with".
* 3.4.5 Fixpoint typing rule: fix fonts for "O" and "S" as 3.4.5 and
  insert spaces as 3.4.2.
* 3.4.5 Fixpoint reduction rule: insert a space between {F} and a_1 for
  consistency.
* 3.4.6 First abstracting property: insert spaces as 3.4.2.

0 files changed, 0 insertions, 0 deletions