Mercurial > cpdt > repo
changeset 495:b7419a10e52e
Pass through Chapter 6
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 20 Jan 2013 06:59:34 -0500 |
parents | 07f2fb4d9b36 |
children | 88688402dc82 |
files | src/Subset.v |
diffstat | 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}% [[