17 Sep
2020
17 Sep
'20
13:00
- 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.
Très bien.
On pourrait par contre garder un symbole pour le nom du type pour imprimer dans les messages d'erreur?
Oui, pour l'instant on va le garder, en attendant d'avoir un meilleur méchanisme pour préserver le nom donné "à l'extérieur".
Stefan