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

comparison src/DataStruct.v @ 463:218361342cd2

Proofreading pass through Chapter 17

author	Adam Chlipala <adam@chlipala.net>
date	Wed, 29 Aug 2012 17:03:19 -0400
parents	b1fead9f68f2
children	1fd4109f7b31

comparison

equal deleted inserted replaced

-:d7a73ab1df7b
+:218361342cd2
 (* begin thide *)
 Variable elm : A.
 Inductive member : list A -> Type :=
-| MFirst : forall ls, member (elm :: ls)
+| HFirst : forall ls, member (elm :: ls)
-| MNext : forall x ls, member ls -> member (x :: ls).
+| HNext : forall x ls, member ls -> member (x :: ls).
 (** Because the element [elm] that we are "searching for" in a list does not change across the constructors of [member], we simplify our definitions by making [elm] a local variable.  In the definition of [member], we say that [elm] is found in any list that begins with [elm], and, if removing the first element of a list leaves [elm] present, then [elm] is present in the original list, too.  The form looks much like a predicate for list membership, but we purposely define [member] in [Type] so that we may decompose its values to guide computations.
 We can use [member] to adapt our definition of [get] to [hlist]s.  The same basic [match] tricks apply.  In the [HCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match].  We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *)
 | HNil => fun mem =>
 match mem in member ls' return (match ls' with
 | nil => B elm
 | _ :: _ => unit
 end) with
-| MFirst _ => tt
+| HFirst _ => tt
-| MNext _ _ _ => tt
+| HNext _ _ _ => tt
 end
 | HCons _ _ x mls' => fun mem =>
 match mem in member ls' return (match ls' with
 | nil => Empty_set
 | x' :: ls'' =>
 B x' -> (member ls'' -> B elm)
 -> B elm
 end) with
-| MFirst _ => fun x _ => x
+| HFirst _ => fun x _ => x
-| MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
+| HNext _ _ mem' => fun _ get_mls' => get_mls' mem'
 end x (hget mls')
 end.
 (* end thide *)
 End hlist.
 (* begin thide *)
 Implicit Arguments HNil [A B].
 Implicit Arguments HCons [A B x ls].
-Implicit Arguments MFirst [A elm ls].
+Implicit Arguments HFirst [A elm ls].
-Implicit Arguments MNext [A elm x ls].
+Implicit Arguments HNext [A elm x ls].
 (* end thide *)
 (** By putting the parameters [A] and [B] in [Type], we allow some very higher-order uses.  For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
 Definition someTypes : list Set := nat :: bool :: nil.
 (* begin thide *)
 Example someValues : hlist (fun T : Set => T) someTypes :=
 HCons 5 (HCons true HNil).
-Eval simpl in hget someValues MFirst.
+Eval simpl in hget someValues HFirst.
 (** %\vspace{-.15in}% [[
 = 5
 : (fun T : Set => T) nat
 ]]
 *)
-Eval simpl in hget someValues (MNext MFirst).
+Eval simpl in hget someValues (HNext HFirst).
 (** %\vspace{-.15in}% [[
 = true
 : (fun T : Set => T) bool
 ]]
 *)
 = tt
 : typeDenote Unit
 ]]
 *)
-Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) HNil.
+Eval simpl in expDenote (Abs (dom := Unit) (Var HFirst)) HNil.
 (** %\vspace{-.15in}% [[
 = fun x : unit => x
 : typeDenote (Arrow Unit Unit)
 ]]
 *)
 Eval simpl in expDenote (Abs (dom := Unit)
-(Abs (dom := Unit) (Var (MNext MFirst)))) HNil.
+(Abs (dom := Unit) (Var (HNext HFirst)))) HNil.
 (** %\vspace{-.15in}% [[
 = fun x _ : unit => x
 : typeDenote (Arrow Unit (Arrow Unit Unit))
 ]]
 *)
-Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) HNil.
+Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var HFirst))) HNil.
 (** %\vspace{-.15in}% [[
 = fun _ x0 : unit => x0
 : typeDenote (Arrow Unit (Arrow Unit Unit))
 ]]
 *)
-Eval simpl in expDenote (App (Abs (Var MFirst)) Const) HNil.
+Eval simpl in expDenote (App (Abs (Var HFirst)) Const) HNil.
 (** %\vspace{-.15in}% [[
 = tt
 : typeDenote Unit
 ]]
 *)

Mercurial > cpdt > repo

comparison src/DataStruct.v @ 463:218361342cd2