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