Certified Programming with Dependent Types: src/Subset.v comparison

comparison src/Subset.v @ 302:7b38729be069

Tweak mark-up to support coqdoc 8.3

author	Adam Chlipala <adam@chlipala.net>
date	Mon, 17 Jan 2011 15:12:30 -0500
parents	b441010125d4
children	d5787b70cf48

comparison

equal deleted inserted replaced

-:f4768d5a75eb
+:7b38729be069
 (** %\vspace{-.15in}% [[
 Notation            Scope
 "{ x : A  |  P }" := sig (fun x : A => P)
 : type_scope
 (default interpretation)
-]] *)
+]]
+*)
 Definition pred_strong2 (s : {n : nat | n > 0}) : nat :=
 match s with
 | exist O pf => match zgtz pf with end
 | exist (S n') _ => n'
 Eval compute in pred_strong2 (exist _ 2 two_gt0).
 (** %\vspace{-.15in}% [[
 = 1
 : nat
-]] *)
+]]
+*)
 Extraction pred_strong2.
 (** %\begin{verbatim}
 (** val pred_strong2 : nat -> nat **)
 Eval compute in pred_strong3 (exist _ 2 two_gt0).
 (** %\vspace{-.15in}% [[
 = exist (fun m : nat => 2 = S m) 1 (refl_equal 2)
 : {m : nat | proj1_sig (exist (lt 0) 2 two_gt0) = S m}
-]] *)
+]]
+*)
 (** The function [proj1_sig] extracts the base value from a subset type.  It turns out that we need to include an explicit [return] clause here, since Coq's heuristics are not smart enough to propagate the result type that we wrote earlier.
 By now, the reader is probably ready to believe that the new [pred_strong] leads to the same OCaml code as we have seen several times so far, and Coq does not disappoint. *)
 Eval compute in pred_strong6 two_gt0.
 (** %\vspace{-.15in}% [[
 = [1]
 : {m : nat | 2 = S m}
-]] *)
+]]
+*)
 (** * 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. *)
 Eval compute in eq_nat_dec 2 2.
 (** %\vspace{-.15in}% [[
 = Yes
 : {2 = 2} + {2 <> 2}
-]] *)
+]]
+*)
 Eval compute in eq_nat_dec 2 3.
 (** %\vspace{-.15in}% [[
 = No
 : {2 = 2} + {2 <> 2}
-]] *)
+]]
+*)
 (** Our definition extracts to reasonable OCaml code. *)
 Extraction eq_nat_dec.
 Eval compute in In_dec eq_nat_dec 2 (1 :: 2 :: nil).
 (** %\vspace{-.15in}% [[
 = Yes
 : {In 2 (1 :: 2 :: nil)} + {~ In 2 (1 :: 2 :: nil)}
-]] *)
+]]
+*)
 Eval compute in In_dec eq_nat_dec 3 (1 :: 2 :: nil).
 (** %\vspace{-.15in}% [[
 = No
 : {In 3 (1 :: 2 :: nil)} + {~ In 3 (1 :: 2 :: nil)}
-]] *)
+]]
+*)
 (** [In_dec] has a reasonable extraction to OCaml. *)
 Extraction In_dec.
 (* end thide *)
 Eval compute in pred_strong7 2.
 (** %\vspace{-.15in}% [[
 = [[1]]
 : {{m | 2 = S m}}
-]] *)
+]]
+*)
 Eval compute in pred_strong7 0.
 (** %\vspace{-.15in}% [[
 = ??
 : {{m | 0 = S m}}
 (** %\vspace{-.15in}% [[
 Inductive sumor (A : Type) (B : Prop) : Type :=
 inleft : A -> A + {B} | inright : B -> A + {B}
 For inleft: Argument A is implicit
 For inright: Argument B is implicit
-]] *)
+]]
+*)
 (** We add notations for easy use of the [sumor] constructors.  The second notation is specialized to [sumor]s whose [A] parameters are instantiated with regular subset types, since this is how we will use [sumor] below. *)
 Notation "!!" := (inright _ _).
 Notation "[[[ x ]]]" := (inleft _ [x]).
 Eval compute in pred_strong8 2.
 (** %\vspace{-.15in}% [[
 = [[[1]]]
 : {m : nat | 2 = S m} + {2 = 0}
-]] *)
+]]
+*)
 Eval compute in pred_strong8 0.
 (** %\vspace{-.15in}% [[
 = !!
 : {m : nat | 0 = S m} + {0 = 0}
-]] *)
+]]
+*)
 (** * Monadic Notations *)
 (** We can treat [maybe] like a monad, in the same way that the Haskell [Maybe] type is interpreted as a failure monad.  Our [maybe] has the wrong type to be a literal monad, but a %``%#"#bind#"#%''%-like notation will still be helpful. *)
 Eval simpl in typeCheck (Nat 0).
 (** %\vspace{-.15in}% [[
 = [[TNat]]
 : {{t | hasType (Nat 0) t}}
-]] *)
+]]
+*)
 Eval simpl in typeCheck (Plus (Nat 1) (Nat 2)).
 (** %\vspace{-.15in}% [[
 = [[TNat]]
 : {{t | hasType (Plus (Nat 1) (Nat 2)) t}}
-]] *)
+]]
+*)
 Eval simpl in typeCheck (Plus (Nat 1) (Bool false)).
 (** %\vspace{-.15in}% [[
 = ??
 : {{t | hasType (Plus (Nat 1) (Bool false)) t}}
-]] *)
+]]
+*)
 (** The type-checker also extracts to some reasonable OCaml code. *)
 Extraction typeCheck.
 Eval simpl in typeCheck' (Nat 0).
 (** %\vspace{-.15in}% [[
 = [[[TNat]]]
 : {t : type | hasType (Nat 0) t} +
 {(forall t : type, ~ hasType (Nat 0) t)}
-]] *)
+]]
+*)
 Eval simpl in typeCheck' (Plus (Nat 1) (Nat 2)).
 (** %\vspace{-.15in}% [[
 = [[[TNat]]]
 : {t : type | hasType (Plus (Nat 1) (Nat 2)) t} +
 {(forall t : type, ~ hasType (Plus (Nat 1) (Nat 2)) t)}
-]] *)
+]]
+*)
 Eval simpl in typeCheck' (Plus (Nat 1) (Bool false)).
 (** %\vspace{-.15in}% [[
 = !!
 : {t : type | hasType (Plus (Nat 1) (Bool false)) t} +
 {(forall t : type, ~ hasType (Plus (Nat 1) (Bool false)) t)}
-]] *)
+]]
+*)
 (** * Exercises *)
 (** All of the notations defined in this chapter, plus some extras, are available for import from the module [MoreSpecif] of the book source.

Mercurial > cpdt > repo

comparison src/Subset.v @ 302:7b38729be069