Mercurial > cpdt > repo

comparison src/DataStruct.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents a913f19955e2
children
comparison
equal deleted inserted replaced
573:c3d77f2bb92c 574:1dc1d41620b6
115 end (get ls') 115 end (get ls')
116 end. 116 end.
117 (* end thide *) 117 (* end thide *)
118 End ilist. 118 End ilist.
119 119
120 Arguments Nil [A]. 120 Arguments Nil {A}.
121 Arguments First [n]. 121 Arguments First {n}.
122 122
123 (** A few examples show how to make use of these definitions. *) 123 (** A few examples show how to make use of these definitions. *)
124 124
125 Check Cons 0 (Cons 1 (Cons 2 Nil)). 125 Check Cons 0 (Cons 1 (Cons 2 Nil)).
126 (** %\vspace{-.15in}% [[ 126 (** %\vspace{-.15in}% [[
240 end. 240 end.
241 (* end thide *) 241 (* end thide *)
242 End hlist. 242 End hlist.
243 243
244 (* begin thide *) 244 (* begin thide *)
245 Arguments HNil [A B]. 245 Arguments HNil {A B}.
246 Arguments HCons [A B x ls] _ _. 246 Arguments HCons [A B x ls] _ _.
247 247
248 Arguments HFirst [A elm ls]. 248 Arguments HFirst {A elm ls}.
249 Arguments HNext [A elm x ls] _. 249 Arguments HNext [A elm x ls] _.
250 (* end thide *) 250 (* end thide *)
251 251
252 (** 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. *) 252 (** 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. *)
253 253
300 | Var : forall ts t, member t ts -> exp ts t 300 | Var : forall ts t, member t ts -> exp ts t
301 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran 301 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
302 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran). 302 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
303 (* end thide *) 303 (* end thide *)
304 304
305 Arguments Const [ts]. 305 Arguments Const {ts}.
306 306
307 (** We write a simple recursive function to translate [type]s into [Set]s. *) 307 (** We write a simple recursive function to translate [type]s into [Set]s. *)
308 308
309 Fixpoint typeDenote (t : type) : Set := 309 Fixpoint typeDenote (t : type) : Set :=
310 match t with 310 match t with