diff options
| author | Hugo Herbelin | 2015-10-06 19:45:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:05 +0100 |
| commit | ba00ffda884142fdd1b4d8b0888d3c9a35457c99 (patch) | |
| tree | 2070653bfb96217183aa0e7a07b1c064b4c58c63 | |
| parent | 779c314c28abbff3d9fc1fca9a2c75dc7e103a1c (diff) | |
RefMan, ch. 4: a few clarifications, thanks to Matej.
There is still something buggy in explaining the interpretation of "match"
as "case": we need typing to reconstruct the types of the x and y1..yn
from the "as x in I ... y1..yn" clause.
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 52003dc34f..aa4483759e 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -497,7 +497,7 @@ The conversion rule is now exactly: \paragraph[Normal form.]{Normal form.\index{Normal form}\label{Normal-form}\label{Head-normal-form}\index{Head normal form}} A term which cannot be any more reduced is said to be in {\em normal form}. There are several ways (or strategies) to apply the reduction -rule. Among them, we have to mention the {\em head reduction} which +rules. Among them, we have to mention the {\em head reduction} which will play an important role (see Chapter~\ref{Tactics}). Any term can be written as $\lb x_1:T_1\mto \ldots \lb x_k:T_k \mto (t_0\ t_1\ldots t_n)$ where @@ -967,7 +967,7 @@ Inductive exType (P:Type->Prop) : Type From {\Coq} version 8.1, inductive families declared in {\Type} are polymorphic over their arguments in {\Type}. -If $A$ is an arity and $s$ a sort, we write $A_{/s}$ for the arity +If $A$ is an arity of some sort and $s$ is a sort, we write $A_{/s}$ for the arity obtained from $A$ by replacing its sort with $s$. Especially, if $A$ is well-typed in some global environment and local context, then $A_{/s}$ is typable by typability of all products in the Calculus of Inductive Constructions. @@ -1260,13 +1260,13 @@ compact notation: \paragraph[Allowed elimination sorts.]{Allowed elimination sorts.\index{Elimination sorts}} An important question for building the typing rule for \kw{match} is -what can be the type of $P$ with respect to the type of the inductive +what can be the type of $\lb a x \mto P$ with respect to the type of the inductive definitions. We define now a relation \compat{I:A}{B} between an inductive definition $I$ of type $A$ and an arity $B$. This relation states that an object in the inductive definition $I$ can be eliminated for -proving a property $P$ of type $B$. +proving a property $\lb a x \mto P$ of type $B$. The case of inductive definitions in sorts \Set\ or \Type{} is simple. There is no restriction on the sort of the predicate to be |