Mercurial > cpdt > repo

comparison src/Generic.v @ 350:ad315efc3b6b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Stub out new chapter
author Adam Chlipala <adam@chlipala.net>
date Wed, 26 Oct 2011 11:19:52 -0400
parents d5787b70cf48
children 6cc9a3bbc2c6
comparison
equal deleted inserted replaced
349:de7db21a016c 350:ad315efc3b6b
75 Variable T : Type. 75 Variable T : Type.
76 (** This variable stands for the concrete datatype that we are interested in. *) 76 (** This variable stands for the concrete datatype that we are interested in. *)
77 77
78 Definition constructorDenote (c : constructor) := 78 Definition constructorDenote (c : constructor) :=
79 nonrecursive c -> ilist T (recursive c) -> T. 79 nonrecursive c -> ilist T (recursive c) -> T.
80 (** We write that a constructor is represented as a function returning a [T]. Such a function takes two arguments, which pack together the non-recursive and recursive arguments of the constructor. We represent a tuple of all recursive arguments using the length-indexed list type [ilist] that we met in Chapter 7. *) 80 (** We write that a constructor is represented as a function returning a [T]. Such a function takes two arguments, which pack together the non-recursive and recursive arguments of the constructor. We represent a tuple of all recursive arguments using the length-indexed list type [ilist] that we met in Chapter 8. *)
81 81
82 Definition datatypeDenote := hlist constructorDenote. 82 Definition datatypeDenote := hlist constructorDenote.
83 (** Finally, the evidence for type [T] is a heterogeneous list, including a constructor denotation for every constructor encoding in a datatype encoding. Recall that, since we are inside a section binding [T] as a variable, [constructorDenote] is automatically parameterized by [T]. *) 83 (** Finally, the evidence for type [T] is a heterogeneous list, including a constructor denotation for every constructor encoding in a datatype encoding. Recall that, since we are inside a section binding [T] as a variable, [constructorDenote] is automatically parameterized by [T]. *)
84 84
85 End denote. 85 End denote.