Stream: Coq devs & plugin devs

Topic: ✔ Weird universe printing due to variance

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 *)

Ali Caglayan (Feb 15 2022 at 23:26):

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

Gaëtan Gilbert (Feb 16 2022 at 08:37):

looks fine, what's the problem?

Ali Caglayan (Feb 16 2022 at 08:40):

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

Gaëtan Gilbert (Feb 16 2022 at 08:41):

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

Gaëtan Gilbert (Feb 16 2022 at 08:41):

preexisting constraints are not printed

Notification Bot (Feb 16 2022 at 09:02):

Ali Caglayan has marked this topic as resolved.

Last updated: Dec 07 2023 at 09:01 UTC