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}% [[