Coq2CLaSH is a library for Coq that contains some verified API functions in order to design circuits in Coq and generate CLaSH code.


# Coq2CLaSH
Coq2CLaSH is a library for the interactive proof assistant [Coq]( that contains some verified CLaSH API functions,
such as the mealy machine. This library needs a special version of Coq that contains the CLaSH language as extraction backend. You find
this version [here]( in the branch: *coq2clash*.

[CLaSH]( is a functional hardware description language embedded in [Haskell](