27 lines
748 B
Coq
27 lines
748 B
Coq
(*
|
|
https://coq.inria.fr/library/Coq.Vectors.VectorDef.html
|
|
https://coq.inria.fr/library/Coq.Bool.Bvector.html
|
|
https://github.com/sifive/Kami/blob/ffb77238f27b603dbd42d2622ba911740bf5eadf/Extraction.v
|
|
|
|
|
|
|
|
https://news.ycombinator.com/item?id=12183095
|
|
|
|
A scala extractor plugin: https://bitbucket.org/yoshihiro503/coq2scala/src/1657d65c747bb9747a4ec32b3da36464631bcd18/coq-8.3pl2/plugins/extraction/scala.ml
|
|
A rust extractor plugin: https://github.com/pirapira/coq2rust/blob/rust/plugins/extraction/rust.ml
|
|
*)
|
|
Require Import Vector.
|
|
Require Import Bvector.
|
|
Import VectorNotations.
|
|
Import BvectorNotations.
|
|
|
|
Definition halfadder (a b: Bvector 1): Bvector 2 :=
|
|
(a ^& b) ++ (a ^⊕ b).
|
|
|
|
|
|
Require Extraction.
|
|
Extraction Language Haskell.
|
|
Extract
|
|
|
|
|