You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
For hs-to-coq to grow into a mighty asset, more community involvement in adding supported libraries could be invaluable.
In the wc example, prior examples containers and transformers are viewed as dependencies (see wc/lib/_CoqProject). This suggests to me that building out the examples dir is one lever to press for
It is my guess that this would be a high-value tutorial to write. If no one's written it by the time I figure out how to do basic hs-to-coq codegen on a small library, I'll certainly write it!
The text was updated successfully, but these errors were encountered:
For hs-to-coq to grow into a mighty asset, more community involvement in adding supported libraries could be invaluable.
I agree!
It is my guess that this would be a high-value tutorial to write. If no one's written it by the time I figure out how to do basic hs-to-coq codegen on a small library, I'll certainly write it!
Let us know if you need any help if you decide to write it :)
For
hs-to-coq
to grow into a mighty asset, more community involvement in adding supported libraries could be invaluable.In the
wc
example, prior examplescontainers
andtransformers
are viewed as dependencies (seewc/lib/_CoqProject
). This suggests to me that building out theexamples
dir is one lever to press forIt is my guess that this would be a high-value tutorial to write. If no one's written it by the time I figure out how to do basic
hs-to-coq
codegen on a small library, I'll certainly write it!The text was updated successfully, but these errors were encountered: