Decidable = typecons (Decidable (prop : Type_ ?ℓ)) (true (p ::: prop)) (false (p ::: Not prop));
Ce qui est élaboré en
Decidable' = lambda (ℓ : TypeLevel) ≡> typecons (Decidable (prop : Type_ ?ℓ)) …
C'est problématique parce que Typer n'élabore pas les lambda dans les datacons. Le code suivant est rejeté parce que Decidable n'est pas un type.
Oui, en fait il y a deux options:
- à l'heure actuelle, Typer ne gère correctement que la définition
Decidable = typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ)) (true (p ::: prop)) (false (p ::: Not prop)); yes = datacons Decidable true; no = datacons Decidable false;
- 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;
- Quelle est la différence sémantique entre les deux formulations?
Aucune, à ma connaissance.
Stefan