ca632cca13
We can declare variables anywhere. So, we must also be able do declare
"universe" variables anywhere. Here is a minimal example that requires
this feature
```
-- We want A and B to be in the same universe
universe variable l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```
The following doesn't work because A and B are in different universes
```
variable A : Type
variable B : Type
definition tst := A = B
```
The following works, but tst is not universe polymorphic, since l is
one *fixed* global universe
```
universe l
variable A : Type.{l}
variable B : Type.{l}
definition tst := A = B
```
5 lines
196 B
Text
5 lines
196 B
Text
id1 : Π (A : Type.{u}), A → A
|
|
id2.{l_2} : Π (B : Type.{l_2}), B → B
|
|
id3.{k} : Π (C : Type.{k}), C → C
|
|
foo.{l} : Π (A₁ A₂ : Type.{l}), A₁ → A₂ → Prop
|
|
Type.{m} : Type.{succ m}
|