Commit graph

4 commits

Author SHA1 Message Date
Sebastian Ullrich
273753f3fc chore(tests): mass-update for pp.binder_types false 2016-06-02 11:28:00 -07:00
Leonardo de Moura
67de3b06f3 feat(kernel/level): improve universe level pretty printer
Example: produce `l+2` instead of `succ (succ l)`.
2014-11-14 14:51:03 -08:00
Leonardo de Moura
6107da05db fix(frontends/lean): universe variable is treated as parameter inside section, fixes #283 2014-10-29 19:47:14 -07:00
Leonardo de Moura
ca632cca13 feat(frontends/lean): add 'universe variable' command
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
```
2014-10-11 14:22:33 -07:00