Re: [Typer] Bug - Types inductifs avec des paramètres dépendants

D’après ce que j’ai compris, le type de `sigma` est

sigma : (A : Type_ ?) ≡> (B : A -> Type_ ?) ≡> (fst : A) -> (snd : B fst) -> Sigma A B;

Puisque le type de `up` a été donné explicitement, c’est à dire

up : Sigma Unit (lambda _ -> Unit);

Je dirais que normalement ça devrait possible de faire l’unification entre `B` et `(lambda _ -> Unit)`?

Ah, oui, j'avais pas fait attention à ce "détail".

J'imagine que c'est un problème qui vient de l'ordre dans lequel on propage l'info. Je te reviens quand j'ai plus de .. détails,

Stefan