content: {-@ LIQUID "--ple" @-}
  -- | Reflection of a function using `quot` and `rem` was not working
  -- because they were not defined in the refinement logic until
  -- https://github.com/ucsd-progsys/liquidhaskell/pull/2540
  -- to fix
  -- https://github.com/ucsd-progsys/liquidhaskell/issues/1447
  
  module QuotRemInt where
  
  {-@ reflect intId @-}
  intId :: Int -> Int
  intId x = (x `quot` 2) * 2 + (x `rem` 2)
  
  {-@ reflect intId' @-}
  intId' :: Int -> Int
  intId' x = (x `div` 2) * 2 + (x `mod` 2)
  
  {-@ lemmaQuotRem :: x:Int -> { intId x = x } @-}
  lemmaQuotRem :: Int -> ()
  lemmaQuotRem _ = ()
  
  {-@ lemmaDivMod :: x:Int -> { intId' x = x } @-}
  lemmaDivMod :: Int -> ()
  lemmaDivMod  _ = ()
  
  {-@
  examplesQuot
     :: { -2 = quot (-5) 2 &&
          -2 = quot 5 (-2) &&
          2 = quot 5 2 &&
          0 = quot 0 2 &&
          0 = quot 1 2 &&
          0 = quot (-1) 2 &&
          2 = quot (-5) (-2) &&
          0 = quot (-1) (-2) &&
          0 = quot 1 (-2)
        }
  @-}
  examplesQuot :: ()
  examplesQuot = ()
  
  {-@
  examplesRem
     :: { -1 = rem (-5) 2 &&
          1 = rem 5 (-2) &&
          1 = rem 5 2 &&
          0 = rem 0 2 &&
          0 = rem 0 (-2) &&
          1 = rem 1 2 &&
          -1 = rem (-1) 2 &&
          -1 = rem (-5) (-2) &&
          -1 = rem (-1) (-2) &&
          1 = rem 1 (-2)
        }
  @-}
  examplesRem :: ()
  examplesRem = ()
  