Stream: Coq devs & plugin devs

Topic: ✔ Weird universe printing due to variance


view this post on Zulip Ali Caglayan (Feb 15 2022 at 23:25):

Set Printing Universes.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.

Inductive Covariant@{+u} : Type@{u}.

Section Univereses.
  Universe u v.
  Constraint u < v. (* <<========= <<<*)
  Axiom co_u : Covariant@{u}.
  Axiom co_v : Covariant@{v}.
  Check (co_u : Covariant@{v}).
  (* co_u : Covariant@{v}
     : Covariant@{v}
(* {} |= u <= v *) wut *)

view this post on Zulip Ali Caglayan (Feb 15 2022 at 23:26):

Is something being printed incorrectly here? cc @Gaëtan Gilbert

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 08:37):

looks fine, what's the problem?

view this post on Zulip Ali Caglayan (Feb 16 2022 at 08:40):

Right but isn't the constraint u < v and not u <= v? Or am I confused?

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 08:41):

u <= v is redundant but that does not stop it from being printed

view this post on Zulip Gaëtan Gilbert (Feb 16 2022 at 08:41):

preexisting constraints are not printed

view this post on Zulip Notification Bot (Feb 16 2022 at 09:02):

Ali Caglayan has marked this topic as resolved.


Last updated: Feb 01 2023 at 15:04 UTC