area/proof-assistantcomponent/typecheckercomponent/unifiergood first issuekind/enhancementmilestone/everest-v1
Metriche repository
- Star
- (3068 star)
- Metriche merge PR
- (Metriche PR in attesa)
Descrizione
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))