errormsggood first issue
Metriche repository
- Star
- (1306 star)
- Metriche merge PR
- (Merge medio 2g 18h) (12 PR mergiate in 30 g)
Descrizione
Hi, I'm trying to represent a function that returns a dependent sum like below
{-@ measure isLeft :: Either a b -> Bool @-}
isLeft (Left _) = True
isLeft (Right _) = False
{-@ example :: x:Int -> {v : Either Int String | (isLeft v && x > 0) || (not (isLeft v) && x <= 0)} @-}
example x =
if x <= 0 then Right "hello" else Left 1
but am running into issues with liquid. Am I representing this correctly? Even without generics, this still doesn't seem to work in the way I might expect.