N. Raghavendra (Gitter import) (Jun 16 2021 at 22:58): N. Raghavendra (Gitter import) (Jun 16 2021 at 22:58):While trying to learn how to use explicit universes, I did something like this:
Set Universe Polymorphism.
Definition constant_function@{l m}
: forall (X : Type@{l}) (Y : Type@{m}), Y -> X -> Y
:= fun (X : Type@{l}) (Y : Type@{m}) (y : Y) (x : X) => y.
Inductive Empty@{l} : Type@{l} := .
Definition empty_function@{l m} : forall (X : Type@{m}), Empty@{l} -> X
:= fun (X : Type@{m}) => Empty_rect (constant_function@{l (m + 1)} Empty@{l} Type@{m} X).
This produces a syntax error on constant_function@{l (m + 1)}. How does one specify the successor of a universe level, or get around doing so? Thanks.
Kenji Maillard (Jun 17 2021 at 06:06):I think you need to add another level m' together with a constraint m < m'. There are restrictions on where arithmetic universe levels (containing successor or max) can be used (see this issue for instance)
N. Raghavendra (Gitter import) (Jun 17 2021 at 06:59):@Kenji Maillard Thanks, yes this works:
Section _empty_function.
Universes l m m'.
Constraint m < m'.
Definition empty_function : forall (X : Type@{m}), Empty@{l} -> X
:= fun (X : Type@{m}) => Empty_rect (constant_function@{l m'} Empty@{l} Type@{m} X).
End _empty_function.
It would be nice if the section could be abbreviated to
Definition empty_function@{l m m' |= m < m'} : forall (X : Type@{m}), Empty@{l} -> X
:= fun (X : Type@{m}) => Empty_rect (constant_function@{l m'} Empty@{l} Type@{m} X).
you can say Definition empty_function@{l m m' | m < m'}
N. Raghavendra (Gitter import) (Jun 17 2021 at 07:18):@Gaëtan Gilbert Thanks, I should have read the GH issue that @Kenji Maillard cited carefully because it has an example of the notation you mentioned. As you say, this works
Definition empty_function@{l m m' | m < m'} : forall (X : Type@{m}), Empty@{l} -> X
:= fun (X : Type@{m}) => Empty_rect (constant_function@{l m'} Empty@{l} Type@{m} X).
Last updated: Sep 23 2023 at 14:01 UTC