Mercurial > cpdt > repo
comparison src/MoreDep.v @ 275:d63cb5fbdce0
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 |