Re: [Typer] Polymorphisme de niveau

• dans le futur (aussi proche que possible, mais je n'ai pas eu beaucoup de temps à y consacrer), Typer n'acceptera probablement que la définition

Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ) = typecons (true (p ::: prop)) (false (p ::: Not prop)); yes (ℓ ::: TypeLevel) (prop ::: Type_ ℓ) = datacons (Decidable prop) true; no (ℓ ::: TypeLevel) (prop ::: Type_ ℓ) = datacons (Decidable prop) false;

Le changement [0] rend possible cette définition, je peux modifier typecons pour ne plus accepter d'arguments. On pourrait par contre garder un symbole pour le nom du type pour imprimer dans les messages d'erreur?

[0]: https://gitlab.com/monnier/typer/-/commit/da12222203e536730456fefc0eaa2f2464...