Mercurial > cpdt > repo

comparison src/MoreDep.v @ 232:d1e0a6d8eef1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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