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

root

# 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/).