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

Coq can have irrefutable patterns in fun args #67

Closed sweirich closed 6 years ago

sweirich commented 6 years ago

We can write

(fun '(x, y, z) => f x y z)

in Gallina. We should do so.