area/proof-assistantcomponent/typecheckercomponent/unifiergood first issuekind/enhancementmilestone/everest-v1
仓库指标
- Star
- (3,068 star)
- PR 合并指标
- (PR 指标待抓取)
描述
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))