hub.darcs.net :: fritjof -> coq2clash -> files

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 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.

  • darcsden 1.2 beta built Jun 23 201810:48:19
  • report problems to simon