# LH/Records/Robin & Klaus

{-@ LIQUID "--exact-data" @-}

foo :: Int -> Int
foo x = x + 1

{-@ reflect bar @-}
bar :: Int -> Int
bar x = foo x

type Record = MkRec
    { x :: {v: Int | pre => v < 0},
    , y :: Int,
    }

type Record = MkRec
    { x :: Int,
    , y :: Int,
    }

type Record_Pre = {r:Record | pre (x r) (y r)}

{-@ inline val @-}
val :: Record -> Bool
val (Record 0 y) = true
val _            = false

{-@ inline val @-}
val = Record { x = 0, y = 0 }

{-@ inline incX @-}
incX record = record { x = x record }