## Mercurial > cpdt > repo

### comparison src/Generic.v @ 504:04177dd1b133

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Pass through Chapter 11

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Sat, 09 Feb 2013 10:45:21 -0500 |

parents | 31258618ef73 |

children | ed829eaa91b2 |

comparison

equal
deleted
inserted
replaced

503:929c12a95b87 | 504:04177dd1b133 |
---|---|

85 (** Finally, the evidence for type [T] is a %\index{Gallina terms!hlist}%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]. *) | 85 (** Finally, the evidence for type [T] is a %\index{Gallina terms!hlist}%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]. *) |

86 | 86 |

87 End denote. | 87 End denote. |

88 (* end thide *) | 88 (* end thide *) |

89 | 89 |

90 (** Some example pieces of evidence should help clarify the convention. First, we define some helpful notations, providing different ways of writing constructor denotations. There is really just one notation, but we need several versions of it to cover different choices of which variables will be used in the body of a definition. %The ASCII \texttt{\textasciitilde{}>} from the notation will be rendered later as $\leadsto$.% *) | 90 (** Some example pieces of evidence should help clarify the convention. First, we define a helpful notation for constructor denotations. %The ASCII \texttt{\textasciitilde{}>} from the notation will be rendered later as $\leadsto$.% *) |

91 | 91 |

92 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)). | |

93 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)). | |

94 Notation "[ ! , r ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ _)). | |

95 Notation "[ v , r ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ _)). | 92 Notation "[ v , r ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ _)). |

96 | 93 |

97 (* begin thide *) | 94 (* begin thide *) |

98 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt := | 95 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt := |

99 HNil. | 96 HNil. |

100 Definition unit_den : datatypeDenote unit unit_dt := | 97 Definition unit_den : datatypeDenote unit unit_dt := |

101 [!, ! ~> tt] ::: HNil. | 98 [_, _ ~> tt] ::: HNil. |

102 Definition bool_den : datatypeDenote bool bool_dt := | 99 Definition bool_den : datatypeDenote bool bool_dt := |

103 [!, ! ~> true] ::: [!, ! ~> false] ::: HNil. | 100 [_, _ ~> true] ::: [_, _ ~> false] ::: HNil. |

104 Definition nat_den : datatypeDenote nat nat_dt := | 101 Definition nat_den : datatypeDenote nat nat_dt := |

105 [!, ! ~> O] ::: [!, r ~> S (hd r)] ::: HNil. | 102 [_, _ ~> O] ::: [_, r ~> S (hd r)] ::: HNil. |

106 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) := | 103 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) := |

107 [!, ! ~> nil] ::: [x, r ~> x :: hd r] ::: HNil. | 104 [_, _ ~> nil] ::: [x, r ~> x :: hd r] ::: HNil. |

108 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) := | 105 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) := |

109 [v, ! ~> Leaf v] ::: [!, r ~> Node (hd r) (hd (tl r))] ::: HNil. | 106 [v, _ ~> Leaf v] ::: [_, r ~> Node (hd r) (hd (tl r))] ::: HNil. |

110 (* end thide *) | 107 (* end thide *) |

111 | 108 |

112 (** Recall that the [hd] and [tl] calls above operate on richly typed lists, where type indices tell us the lengths of lists, guaranteeing the safety of operations like [hd]. The type annotation attached to each definition provides enough information for Coq to infer list lengths at appropriate points. *) | 109 (** Recall that the [hd] and [tl] calls above operate on richly typed lists, where type indices tell us the lengths of lists, guaranteeing the safety of operations like [hd]. The type annotation attached to each definition provides enough information for Coq to infer list lengths at appropriate points. *) |

113 | 110 |

114 | 111 |