Mercurial > cpdt > repo

comparison src/MoreDep.v @ 275:d63cb5fbdce0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A suggestion from sbriais: mention that Coq >=8.2 allows omitted match cases
author Adam Chlipala <adam@chlipala.net>
date Mon, 28 Jun 2010 07:59:01 -0400
parents d1e0a6d8eef1
children 756ce68e42fb
comparison
equal deleted inserted replaced
274:806420cf7a2f 275:d63cb5fbdce0
119 119
120 Error: Non exhaustive pattern-matching: no clause found for pattern Nil 120 Error: Non exhaustive pattern-matching: no clause found for pattern Nil
121 121
122 ]] 122 ]]
123 123
124 Unlike in ML, we cannot use inexhaustive pattern matching, because there is no conception of a %\texttt{%#<tt>#Match#</tt>#%}% exception to be thrown. We might try using an [in] clause somehow. 124 Unlike in ML, we cannot use inexhaustive pattern matching, because there is no conception of a %\texttt{%#<tt>#Match#</tt>#%}% exception to be thrown. In fact, recent versions of Coq %\textit{%#<i>#do#</i>#%}% allow this, by implicit translation to a [match] that considers all constructors. It is educational to discover that encoding ourselves directly. We might try using an [in] clause somehow.
125 125
126 [[ 126 [[
127 Definition hd n (ls : ilist (S n)) : A := 127 Definition hd n (ls : ilist (S n)) : A :=
128 match ls in (ilist (S n)) with 128 match ls in (ilist (S n)) with
129 | Cons _ h _ => h 129 | Cons _ h _ => h