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

"Non-function top level binding unsupported" #81

Open sweirich opened 6 years ago

sweirich commented 6 years ago

We can't say:

(x,y) = (True,False)

This occurs in PrelNames, but low priority. We probably want to manually axiomatize this module anyways. Just making the issue to mark this as an unsupported feature.

I'll push a new test case tests/TopBind.hs

nomeata commented 6 years ago

I guess since of my recent refactoring made that even harder, now that the types enforce that expressions are translated in the context of exactly one local function name. Maybe it could be relaxed to a list of functions.