Mercurial > cpdt > repo

comparison src/Subset.v @ 294:1b6c81e51799

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixes added while proofreading JFR camera-ready
author Adam Chlipala <adam@chlipala.net>
date Thu, 09 Dec 2010 13:44:57 -0500
parents 2c88fc1dbe33
children b441010125d4
comparison
equal deleted inserted replaced
293:e2dbc0f1c1e8 294:1b6c81e51799
82 = 1 82 = 1
83 : nat 83 : nat
84 84
85 ]] 85 ]]
86 86
87 One aspect in particular of the definition of [pred_strong1] may be surprising. We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions. Let us see what happens if we write this function in the way that at first seems most natural. 87 One aspect in particular of the definition of [pred_strong1] may be surprising. We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions. Let us see what happens if we write this function in the way that at first seems most natural.
88 88
89 [[ 89 [[
90 Definition pred_strong1' (n : nat) (pf : n > 0) : nat := 90 Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=
91 match n with 91 match n with
92 | O => match zgtz pf with end 92 | O => match zgtz pf with end