Janno (Apr 06 2021 at 09:38): Janno (Apr 06 2021 at 09:38):Coq introduces a universe constraint Set < u in the definition below and I don't understand why it adds this constraint. Is it not implied by u0 < u (which is the second constraint Coq generates)? Both u := Prop and u := Set suffice to conclude u >= Set+1, AFAICT.
Definition type_or_prop@{u u0} (b : bool) : Type@{u} :=
if b then Prop else Type@{u0}.
(* {type_or_prop.u0 type_or_prop.u} |= Set < type_or_prop.u
type_or_prop.u0 < type_or_prop.u *)
monomorphic univs are always declared > Set
Janno (Apr 06 2021 at 10:03):u0 is not > Set, is it?
Gaëtan Gilbert (Apr 06 2021 at 10:04):actually it is, but the implicit > Set is not listed (being implicit)
Gaëtan Gilbert (Apr 06 2021 at 10:05):also Coq does not especially try to remove redundant constraints
Janno (Apr 06 2021 at 10:06):Hm. So what decides whether a > Set constraint is implicit or explicit, i.e. printed?
Gaëtan Gilbert (Apr 06 2021 at 10:09):some magic
I recommend not caring
Janno (Apr 06 2021 at 10:14):Okay, I'll try to not care about that. :)
Last updated: Sep 30 2023 at 05:01 UTC