Bonjour, Decidable est définit comme suit 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. yes = datacons Decidable true; Je propose le changement [0], qui instancie les arguments implicites dans les datacons, mais plus j'y pense, plus je me rends compte que ce n'est pas la bonne solution à ce problème. (Je pense quand même que ce changement est correct, mais pour d'autres circonstances.) Decidable ne devrait-il pas être définit comme Decidable'' = typecons (Decidable (ℓ ::: TypeLevel) (t : Type_ ℓ)) … Mes deux questions sont: - Quelle est la différence sémantique entre les deux formulations? - Si la première est incorrecte, est-ce que l'élaboration des typecons devrait être changé pour que l'élaboration du code le plus naturel donne "la bonne chose". Bon typage Simon [0]: https://gitlab.com/monnier/typer/-/commit/da12222203e536730456fefc0eaa2f2464...