Stream: Coq users

Topic: bypass universe check

Ali Caglayan (Oct 12 2021 at 09:31):

I have a definition with a universe inconsistency. I would like to bypass the check but the attribute doesn't seem to work. Any ideas what I might be doing wrong?

Axiom Ty : Type.
Axiom ty_zero : Ty.
Axiom ty_sum : Ty -> Ty -> Ty.
Axiom Ctx : Type.
Axiom ctx_exten : Ctx -> Ty -> Ctx.
Axiom Ne : Ty -> Ctx -> Type.

(* #[bypass_check(universes)] *)
Inductive Cov@{u} : (Ctx -> Type@{u}) -> Ctx -> Type@{u} :=
| cov_return {A} {Γ} : A Γ -> Cov A Γ
| cov_abort {A} Γ : Ne ty_zero Γ -> Cov A Γ
| cov_case {A B C} Γ
  : Ne (ty_sum A B) Γ -> Cov C (ctx_exten Γ A) -> Cov C (ctx_exten Γ B)
  -> Cov C Γ
.

Ali Caglayan (Oct 12 2021 at 09:32):

It complains that I have an unbound universe if I pass the attribute

Gaëtan Gilbert (Oct 12 2021 at 09:53):

unbound universe means that the list in @{u} is not complete, it's orthogonal to bypass_check
you can do @{u +} to say that incompleteness is allowed

Ali Caglayan (Oct 12 2021 at 11:05):

Nice, thanks!

Last updated: Sep 23 2023 at 13:01 UTC