diff options
Diffstat (limited to 'doc/refman/RefMan-gal.tex')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index cf83d0c72..9b527053c 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -587,6 +587,9 @@ is a variable, the {\tt as} clause can be omitted and the term being matched can serve itself as binding name in the return type. For instance, the following alternative definition is accepted and has the same meaning as the previous one. +\begin{coq_eval} +Reset bool_case. +\end{coq_eval} \begin{coq_example*} Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := match b return or (eq bool b true) (eq bool b false) with @@ -623,7 +626,7 @@ For instance, in the following example: \begin{coq_example*} Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := match H in eq _ _ z return eq A z x with - | eq_refl => eq_refl A x + | eq_refl _ _ => eq_refl A x end. \end{coq_example*} the type of the branch has type {\tt eq~A~x~x} because the third @@ -1120,7 +1123,7 @@ This is an alternative definition of lists where we specify the arguments of the constructors rather than their full type. \item \begin{coq_example*} -Variant sum (A B:Set) : Set := left : A->sum A B | right : B->Sum A B. +Variant sum (A B:Set) : Set := left : A -> sum A B | right : B -> sum A B. \end{coq_example*} The {\tt Variant} keyword is identical to the {\tt Inductive} keyword, except that it disallows recursive definition of types (in particular |