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

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

looks fine, what's the problem?

Right but isn't the constraint `u < v`

and not `u <= v`

? Or am I confused?

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

preexisting constraints are not printed

Ali Caglayan has marked this topic as resolved.

Last updated: Dec 07 2023 at 09:01 UTC