Mercurial > cpdt > repo

comparison src/Generic.v @ 215:f8bcd33bdd91

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port DataStruct
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 14:00:04 -0500
parents a35eaec19781
children d1464997078d
comparison
equal deleted inserted replaced
214:768889c969e9 215:f8bcd33bdd91
215 Variable fx : fixDenote T dt. 215 Variable fx : fixDenote T dt.
216 216
217 Definition datatypeDenoteOk := 217 Definition datatypeDenoteOk :=
218 forall P : T -> Prop, 218 forall P : T -> Prop,
219 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)), 219 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
220 (forall i : index (recursive c), P (get r i)) 220 (forall i : fin (recursive c), P (get r i))
221 -> P ((hget dd m) x r)) 221 -> P ((hget dd m) x r))
222 -> forall v, P v. 222 -> forall v, P v.
223 223
224 Definition fixDenoteOk := 224 Definition fixDenoteOk :=
225 forall (R : Type) (cases : datatypeDenote R dt) 225 forall (R : Type) (cases : datatypeDenote R dt)