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

comparison src/DataStruct.v @ 569:0ce9829efa3b

Back to working in Coq 8.4

author	Adam Chlipala <adam@chlipala.net>
date	Sun, 20 Jan 2019 15:28:23 -0500
parents	81d63d9c1cc5
children	a913f19955e2

comparison

equal deleted inserted replaced

-:81d63d9c1cc5
+:0ce9829efa3b
 (* end thide *)
 End hlist.
 (* begin thide *)
 Arguments HNil [A B].
-Arguments HCons [A B x ls].
+Arguments HCons [A B x ls] _ _.
 Arguments HFirst [A elm ls].
-Arguments HNext [A elm x ls].
+Arguments HNext [A elm x ls] _.
 (* end thide *)
 (** By putting the parameters [A] and [B] in [Type], we enable fancier kinds of polymorphism than in mainstream functional languages.  For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
 Definition someTypes : list Set := nat :: bool :: nil.
 In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument.  The type of the constructor [eq_refl] shows that [y] can only ever be instantiated to [x].  Thus, within a pattern-match with [eq_refl], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *)
 (* end thide *)
 End fhlist.
-Arguments fhget [A B elm ls].
+Arguments fhget [A B elm ls] _ _.
 (** How does one choose between the two data structure encoding strategies we have presented so far?  Before answering that question in this chapter's final section, we introduce one further approach. *)
 (** * Data Structures as Index Functions *)
 (** A [Node] is indexed by a natural number [n], and the node's [n] children are represented as a function from [ffin n] to trees, which is isomorphic to the [ilist]-based representation that we used above. *)
 End tree.
-Arguments Node [A n].
+Arguments Node [A n] _.
 (** We can redefine [sum] and [inc] for our new [tree] type.  Again, it is useful to define a generic fold function first.  This time, it takes in a function whose domain is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *)
 Section rifoldr.
 Variables A B : Set.
 | O => fun _ => i
 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx)))
 end.
 End rifoldr.
-Arguments rifoldr [A B] f i [n].
+Arguments rifoldr [A B] f i [n] _.
 Fixpoint sum (t : tree nat) : nat :=
 match t with
 | Leaf n => n
 | Node _ f => rifoldr plus O (fun idx => sum (f idx))
 (fun idx => tests (Some idx))
 (fun idx => bodies (Some idx))
 end.
 End cond.
-Arguments cond [A] default [n].
+Arguments cond [A] default [n] _ _.
 (* end thide *)
 (** Now the expression interpreter is straightforward to write. *)
 (* begin thide *)
 end (bodies None)
 end
 end.
 End cfoldCond.
-Arguments cfoldCond [t] default [n].
+Arguments cfoldCond [t] default [n] _ _.
 (* end thide *)
 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
 (* begin thide *)

Mercurial > cpdt > repo

comparison src/DataStruct.v @ 569:0ce9829efa3b