area/proof-assistantcomponent/typecheckercomponent/unifiergood first issuekind/enhancementmilestone/everest-v1
Repository metrics
- Stars
- (3,068 stars)
- PR merge metrics
- (PR metrics pending)
説明
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))