Extractionという機能を使うとできるらしい。Coqで証明してHaskellで動作させる感じなのか。 coq.inria.fr 単純な方の定義 Inductive FBB : Type := | Foo | Bar | Buzz. Require Extraction. Extraction Language Haskell. Extraction "C:\work\FBB.hs" FBB…