diff options
| author | Matej Kosik | 2015-11-10 09:11:50 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:19 +0100 |
| commit | 32bd14114d5137b917601092730469db569d6385 (patch) | |
| tree | b416c7da024ad1401da727dbf22cdd1a8a6a8aae | |
| parent | 5e48f1aafb45d1c883e32e13a8458979663b04fb (diff) | |
PROPOSITION: Added an explicit definition of the notation for enriching the global environment (we use throughout the document)
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 6c1417a7f2..2781b4cbe5 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -257,6 +257,10 @@ A {\em global definition} will be represented in the global environment as $c:=t:T$ which defines the name $c$ to have value $t$ and type $T$. We shall call such names {\em constants}. +For the rest of the chapter, the $E;c:T$ denotes the global environment +$E$ enriched with the global assumption $c:T$. +Similarly, $E;c:=t:T$ denotes the global environment +$E$ enriched with the global definition $(c:=t:T)$. The rules for inductive definitions (see Section \ref{Cic-inductive-definitions}) have to be considered as assumption |