diff options
| -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 |