search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

hs-to-coq doesn't accept minimal implementation of Ord in terms of (<=) #116

Closed emarzion closed 6 years ago

emarzion commented 6 years ago

The following code is rejected by hs-to-coq with the error message The method `GHC.Base.compare' has no definition and no default definition :

module Test where

data Test = A | B deriving Eq

instance Ord Test where
  A <= _ = True
  B <= B = True
  _ <= _ = False
sweirich commented 6 years ago

Ord is treated specially by hs-to-coq (and by GHC). I'm adding a default definition for GHC.Base.compare to https://github.com/antalsz/hs-to-coq/blob/master/src/lib/HsToCoq/ConvertHaskell/BuiltIn.hs now.