Library ExtractionNoCubes

Require Import CubeAndConquer.
Require Import SetChecker.

Extraction Language Ocaml.

Extract Inductive positive => int [ "(fun x -> 2*x+1)" "(fun x -> 2*x)" "1" ]
 "(fun fI fO fH n -> if n=1 then fH () else if n mod 2 = 0 then fO (n/2) else fI (n/2))".

Extract Inlined Constant Pos.compare => "(fun x y -> if x = y then Eq else (if x < y then Lt else Gt))".

Extract Inductive nat => int [ "0" "Pervasives.succ" ]
 "(fun fO fS n -> if n=0 then fO () else fS (n-1))".

Extract Inlined Constant force => "Lazy.force".
Extract Inlined Constant fromVal => "Lazy.from_val".
Extract Constant LazyT "'a" => "'a Lazy.t".

Extraction "Coq" noCube refute.