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: May 28 2023 at 13:30 UTC