area/proof-assistantcomponent/typecheckercomponent/unifiergood first issuekind/enhancementmilestone/everest-v1
Métriques du dépôt
- Stars
- (3 068 stars)
- Métriques de merge PR
- (Métriques PR en attente)
Description
Lax-typechecking the following snippet
let f (x y : int) (w:(b:bool & (if b then equals x y else equals y x))) =
match w with
| (| b, Refl |) -> ()
fails with the error
(Error) (equals (?26524 x y w b) (?26524 x y w b)) is not a subtype of the expected type (match b with
| true -> (equals x y)
|_ -> (equals y x))