content: -- TODO-REBARE-CLASS: does not support this `define` hack, which should be supported properly.
  
  {-@ LIQUID "--reflection"     @-}
  
  module Nat where
  
  import Language.Haskell.Liquid.ProofCombinators
  
  
  {-@ data N [toInt] = Zero | Suc N @-}
  data N = Zero | Suc N
  
  {-@ measure toInt @-}
  {-@ toInt :: N -> Nat @-}
  toInt :: N -> Int
  toInt Zero = 0
  toInt (Suc n) = 1 + toInt n
  
  {-@ class VerifiedEq a where
        eq :: a -> a -> Bool
        refl :: x:a -> { v:Proof | eq x x }
    @-}
  class Eq a => VerifiedEq a where
    eq   :: a -> a -> Bool 
    eq = (==)
    refl :: a -> Proof
  
  
  {-@ axiomatize eqN  @-}
  eqN :: N -> N -> Bool
  eqN Zero    Zero = True
  eqN (Suc m) (Suc n) = eqN m n
  eqN _ _ = False
  
  {-@ eqNRefl :: x:N -> { eqN x x } @-}
  eqNRefl :: N -> Proof
  eqNRefl Zero =   eqN Zero Zero
               === True
               *** QED
  eqNRefl (Suc n) =   eqN (Suc n) (Suc n)
                  === eqN n n
                  ==? True ? eqNRefl n
                  *** QED
  
  instance Eq N where
    (==) = eqN  
  
  instance VerifiedEq N where
    -- This define should derive automatically
    {-@ define $ceq = eqN @-}
    refl = eqNRefl
  
  