diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-06 16:58:22 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:17 +0100 |
commit | 56abd3ce281e3fd8f3df27597c6348d6ab033b64 (patch) | |
tree | 8409dbe25ec25c5d209612baa7b5db337b585595 /doc/refman | |
parent | f7051cd4eb4cefc4b2ec04c8c29369dcaf0062f2 (diff) |
ENH: existing example was expanded
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/RefMan-cic.tex | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 91c141854..d2bae76f6 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1584,9 +1584,12 @@ branch corresponding to the $c:C$ constructor. We write \CI{c}{P} for \CI{c:C}{P} with $C$ the type of $c$. \paragraph{Examples.} -For $\List \nat$ the type of $P$ will be $\ListA\ra s$ for $s \in \Sort$. \\ -$ \CI{(\cons~A)}{P} \equiv -\forall a:A, \forall l:\ListA,(P~(\cons~A~a~l))$. +For $\List~\nat$ the type of $P$ will be $\List~\nat\ra s$ for $s \in \Sort$. \\ +$ \CI{(\cons~\nat)}{P} + \equiv\CI{(\cons~\nat) : (\nat\ra\List~\nat\ra\List~\nat)}{P} \equiv\\ + \equiv\forall n:\nat, \CI{(\cons~\nat~n) : \List~\nat\ra\List~\nat)}{P} \equiv\\ + \equiv\forall n:\nat, \forall l:\List~\nat, \CI{(\cons~\nat~n~l) : \List~\nat)}{P} \equiv\\ +\equiv\forall n:\nat, \forall l:\List~\nat,(P~(\cons~\nat~n~l))$. For $\haslengthA$, the type of $P$ will be $\forall l:\ListA,\forall n:\nat, (\haslengthA~l~n)\ra \Prop$ and the expression |