Mercurial > cpdt > repo

comparison src/Subset.v @ 338:c7faf3551c5d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass over MoreDep
author Adam Chlipala <adam@chlipala.net>
date Mon, 10 Oct 2011 16:01:31 -0400
parents 4186722d329b
children aaeba4cfd075
comparison
equal deleted inserted replaced
337:4186722d329b 338:c7faf3551c5d
324 exist (fun m : nat => S n' = S m) n' (pred_strong4'_subproof0 n _H) 324 exist (fun m : nat => S n' = S m) n' (pred_strong4'_subproof0 n _H)
325 end 325 end
326 : forall n : nat, n > 0 -> {m : nat | n = S m} 326 : forall n : nat, n > 0 -> {m : nat | n = S m}
327 ]] 327 ]]
328 328
329 We are almost done with the ideal implementation of dependent predecessor. We can use Coq's syntax extension facility to arrive at code with almost no complexity beyond a Haskell or ML program with a complete specification in a comment. *) 329 We are almost done with the ideal implementation of dependent predecessor. We can use Coq's syntax extension facility to arrive at code with almost no complexity beyond a Haskell or ML program with a complete specification in a comment. In this book, we will not dwell on the details of syntax extensions; the Coq manual gives a straightforward introduction to them. *)
330 330
331 Notation "!" := (False_rec _ _). 331 Notation "!" := (False_rec _ _).
332 Notation "[ e ]" := (exist _ e _). 332 Notation "[ e ]" := (exist _ e _).
333 333
334 Definition pred_strong5 : forall n : nat, n > 0 -> {m : nat | n = S m}. 334 Definition pred_strong5 : forall n : nat, n > 0 -> {m : nat | n = S m}.