Mercurial > cpdt > repo

comparison src/Universes.v @ 417:539ed97750bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for Coq trunk version intended for final 8.4 release
author Adam Chlipala <adam@chlipala.net>
date Tue, 17 Jul 2012 16:37:58 -0400
parents 934945edc6b5
children 686cf945dd02
comparison
equal deleted inserted replaced
416:ded318830bb0 417:539ed97750bb
236 Error: Universe inconsistency (cannot enforce Top.42 < Top.42). 236 Error: Universe inconsistency (cannot enforce Top.42 < Top.42).
237 >> 237 >>
238 238
239 We are unable to instantiate the parameter [T] of [Const] with an [exp] type. To see why, it is helpful to print the annotated version of [exp]'s inductive definition. *) 239 We are unable to instantiate the parameter [T] of [Const] with an [exp] type. To see why, it is helpful to print the annotated version of [exp]'s inductive definition. *)
240 240
241 (** [[
241 Print exp. 242 Print exp.
242 (** %\vspace{-.15in}% [[ 243 ]]
244
245 [[
243 Inductive exp 246 Inductive exp
244 : Type $ Top.8 ^ -> 247 : Type $ Top.8 ^ ->
245 Type 248 Type
246 $ max(0, (Top.11)+1, (Top.14)+1, (Top.15)+1, (Top.19)+1) ^ := 249 $ max(0, (Top.11)+1, (Top.14)+1, (Top.15)+1, (Top.19)+1) ^ :=
247 Const : forall T : Type $ Top.11 ^ , T -> exp T 250 Const : forall T : Type $ Top.11 ^ , T -> exp T
266 269
267 The command outputs many more constraints, but we have collected only those that mention [Top] variables. We see one constraint for each universe variable associated with a constructor argument from [exp]'s definition. Universe variable [Top.19] is the type argument to [Eq]. The constraint for [Top.19] effectively says that [Top.19] must be less than [Top.8], the universe of [exp]'s indices; an intermediate variable [Top.9] appears as an artifact of the way the constraint was generated. 270 The command outputs many more constraints, but we have collected only those that mention [Top] variables. We see one constraint for each universe variable associated with a constructor argument from [exp]'s definition. Universe variable [Top.19] is the type argument to [Eq]. The constraint for [Top.19] effectively says that [Top.19] must be less than [Top.8], the universe of [exp]'s indices; an intermediate variable [Top.9] appears as an artifact of the way the constraint was generated.
268 271
269 The next constraint, for [Top.15], is more complicated. This is the universe of the second argument to the [Pair] constructor. Not only must [Top.15] be less than [Top.8], but it also comes out that [Top.8] must be less than [Coq.Init.Datatypes.38]. What is this new universe variable? It is from the definition of the [prod] inductive family, to which types of the form [A * B] are desugared. *) 272 The next constraint, for [Top.15], is more complicated. This is the universe of the second argument to the [Pair] constructor. Not only must [Top.15] be less than [Top.8], but it also comes out that [Top.8] must be less than [Coq.Init.Datatypes.38]. What is this new universe variable? It is from the definition of the [prod] inductive family, to which types of the form [A * B] are desugared. *)
270 273
274 (* begin hide *)
275 Inductive prod := pair.
276 Reset prod.
277 (* end hide *)
278
279 (** [[
271 Print prod. 280 Print prod.
272 (** %\vspace{-.15in}% [[ 281 ]]
282
283 [[
273 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ ) 284 Inductive prod (A : Type $ Coq.Init.Datatypes.37 ^ )
274 (B : Type $ Coq.Init.Datatypes.38 ^ ) 285 (B : Type $ Coq.Init.Datatypes.38 ^ )
275 : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ := 286 : Type $ max(Coq.Init.Datatypes.37, Coq.Init.Datatypes.38) ^ :=
276 pair : A -> B -> A * B 287 pair : A -> B -> A * B
277 288