## Mercurial > cpdt > repo

### comparison src/Universes.v @ 488:31258618ef73

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

Incorporate feedback from Nathan Collins

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

date | Tue, 08 Jan 2013 14:38:56 -0500 |

parents | 40a9a36844d6 |

children | 2036ef0bc891 |

comparison

equal
deleted
inserted
replaced

487:8bfb27cf0121 | 488:31258618ef73 |
---|---|

89 | 89 |

90 Occurrences of [Type] are annotated with some additional information, inside comments. These annotations have to do with the secret behind [Type]: it really stands for an infinite hierarchy of types. The type of [Set] is [Type(0)], the type of [Type(0)] is [Type(1)], the type of [Type(1)] is [Type(2)], and so on. This is how we avoid the "[Type : Type]" paradox. As a convenience, the universe hierarchy drives Coq's one variety of subtyping. Any term whose type is [Type] at level [i] is automatically also described by [Type] at level [j] when [j > i]. | 90 Occurrences of [Type] are annotated with some additional information, inside comments. These annotations have to do with the secret behind [Type]: it really stands for an infinite hierarchy of types. The type of [Set] is [Type(0)], the type of [Type(0)] is [Type(1)], the type of [Type(1)] is [Type(2)], and so on. This is how we avoid the "[Type : Type]" paradox. As a convenience, the universe hierarchy drives Coq's one variety of subtyping. Any term whose type is [Type] at level [i] is automatically also described by [Type] at level [j] when [j > i]. |

91 | 91 |

92 In the outputs of our first [Check] query, we see that the type level of [Set]'s type is [(0)+1]. Here [0] stands for the level of [Set], and we increment it to arrive at the level that _classifies_ [Set]. | 92 In the outputs of our first [Check] query, we see that the type level of [Set]'s type is [(0)+1]. Here [0] stands for the level of [Set], and we increment it to arrive at the level that _classifies_ [Set]. |

93 | 93 |

94 In the second query's output, we see that the occurrence of [Type] that we check is assigned a fresh%\index{universe variable}% _universe variable_ [Top.3]. The output type increments [Top.3] to move up a level in the universe hierarchy. As we write code that uses definitions whose types mention universe variables, unification may refine the values of those variables. Luckily, the user rarely has to worry about the details. | 94 In the third query's output, we see that the occurrence of [Type] that we check is assigned a fresh%\index{universe variable}% _universe variable_ [Top.3]. The output type increments [Top.3] to move up a level in the universe hierarchy. As we write code that uses definitions whose types mention universe variables, unification may refine the values of those variables. Luckily, the user rarely has to worry about the details. |

95 | 95 |

96 Another crucial concept in CIC is%\index{predicativity}% _predicativity_. Consider these queries. *) | 96 Another crucial concept in CIC is%\index{predicativity}% _predicativity_. Consider these queries. *) |

97 | 97 |

98 Check forall T : nat, fin T. | 98 Check forall T : nat, fin T. |

99 (** %\vspace{-.15in}% [[ | 99 (** %\vspace{-.15in}% [[ |