Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/DataStruct.v Sun Jan 20 15:16:29 2019 -0500 +++ b/src/DataStruct.v Sun Jan 20 15:28:23 2019 -0500 @@ -243,10 +243,10 @@ (* 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. *) @@ -481,7 +481,7 @@ 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. *) @@ -592,7 +592,7 @@ 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. *) @@ -608,7 +608,7 @@ 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 @@ -708,7 +708,7 @@ end. End cond. -Arguments cond [A] default [n]. +Arguments cond [A] default [n] _ _. (* end thide *) (** Now the expression interpreter is straightforward to write. *) @@ -797,7 +797,7 @@ 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. *)