### changeset 495:b7419a10e52e

Pass through Chapter 6
author Adam Chlipala Sun, 20 Jan 2013 06:59:34 -0500 07f2fb4d9b36 88688402dc82 src/Subset.v 1 files changed, 11 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/Subset.v	Sat Jan 19 10:45:04 2013 -0500
+++ b/src/Subset.v	Sun Jan 20 06:59:34 2013 -0500
@@ -161,9 +161,9 @@

Locate "{ _ : _ | _ }".
(** %\vspace{-.15in}% [[
-Notation
-"{ x : A  |  P }" := sig (fun x : A => P)
- ]]
+  Notation
+  "{ x : A  |  P }" := sig (fun x : A => P)
+   ]]
*)

Definition pred_strong2 (s : {n : nat | n > 0}) : nat :=
@@ -209,6 +209,12 @@
| exist (S n') pf => exist _ n' (eq_refl _)
end.

+(* begin hide *)
+(* begin thide *)
+Definition ugh := lt.
+(* end thide *)
+(* end hide *)
+
Eval compute in pred_strong3 (exist _ 2 two_gt0).
(** %\vspace{-.15in}% [[
= exist (fun m : nat => 2 = S m) 1 (eq_refl 2)
@@ -370,7 +376,7 @@
| S n' => n'
end.

-(** Printing the resulting definition of [pred_strong6] yields a term very similar to what we built with [refine].  [Program] can save time in writing programs that use subset types.  Nonetheless, [refine] is often just as effective, and [refine] gives you more control over the form the final term takes, which can be useful when you want to prove additional theorems about your definition.  [Program] will sometimes insert type casts that can complicate theorem proving. *)
+(** Printing the resulting definition of [pred_strong6] yields a term very similar to what we built with [refine].  [Program] can save time in writing programs that use subset types.  Nonetheless, [refine] is often just as effective, and [refine] gives more control over the form the final term takes, which can be useful when you want to prove additional theorems about your definition.  [Program] will sometimes insert type casts that can complicate theorem proving. *)

Eval compute in pred_strong6 two_gt0.
(** %\vspace{-.15in}% [[
@@ -383,7 +389,7 @@

(** * Decidable Proposition Types *)

-(** There is another type in the standard library which captures the idea of program values that indicate which of two propositions is true.%\index{Gallina terms!sumbool}% *)
+(** There is another type in the standard library that captures the idea of program values that indicate which of two propositions is true.%\index{Gallina terms!sumbool}% *)

Print sumbool.
(** %\vspace{-.15in}% [[