Mercurial > cpdt > repo
comparison src/MoreDep.v @ 232:d1e0a6d8eef1
Fix typo
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 24 Nov 2009 07:54:38 -0500 |
parents | 768889c969e9 |
children | d63cb5fbdce0 |
comparison
equal
deleted
inserted
replaced
231:bc0f515a929f | 232:d1e0a6d8eef1 |
---|---|
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, becuase 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. 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 |