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

Axiomatizing methods #57

Closed lastland closed 5 years ago

lastland commented 6 years ago

Right now hs-to-coq only supports axiomatizing modules. It would be good if we can axiomatize only some certain methods inside a module.

nomeata commented 6 years ago

With methods, I assume you mean functions?

antalsz commented 5 years ago

We can now axiomatize definition – closing.