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 Γ
.
```

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

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

Nice, thanks!

Last updated: Jun 16 2024 at 01:42 UTC