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

comparison src/DataStruct.v @ 568:81d63d9c1cc5

Port to Coq 8.9.0

author	Adam Chlipala <adam@chlipala.net>
date	Sun, 20 Jan 2019 15:16:29 -0500
parents	ed829eaa91b2
children	0ce9829efa3b

comparison

equal deleted inserted replaced

-:ec0ce5129fc4
+:81d63d9c1cc5
 end (get ls')
 end.
 (* end thide *)
 End ilist.
-Implicit Arguments Nil [A].
+Arguments Nil [A].
-Implicit Arguments First [n].
+Arguments First [n].
 (** A few examples show how to make use of these definitions. *)
 Check Cons 0 (Cons 1 (Cons 2 Nil)).
 (** %\vspace{-.15in}% [[
 end.
 (* end thide *)
 End hlist.
 (* begin thide *)
-Implicit Arguments HNil [A B].
+Arguments HNil [A B].
-Implicit Arguments HCons [A B x ls].
+Arguments HCons [A B x ls].
-Implicit Arguments HFirst [A elm ls].
+Arguments HFirst [A elm ls].
-Implicit 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.
 | Var : forall ts t, member t ts -> exp ts t
 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
 (* end thide *)
-Implicit Arguments Const [ts].
+Arguments Const [ts].
 (** We write a simple recursive function to translate [type]s into [Set]s. *)
 Fixpoint typeDenote (t : type) : Set :=
 match t with
 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.
-Implicit 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.
-Implicit 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.
-Implicit Arguments rifoldr [A B 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.
-Implicit Arguments cond [A 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.
-Implicit Arguments cfoldCond [t 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 @ 568:81d63d9c1cc5