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](https://coq.inria.fr/) 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](https://gitlab.informatik.uni-bremen.de/fritjof/coq) in the branch: *coq2clash*. [CLaSH](https://clash-lang.org/) is a functional hardware description language embedded in [Haskell](https://www.haskell.org/).