Library Extraction

Require Export Prune.

Extraction Language Haskell.

Extract Inductive bool => Bool [ True False ].

NB: The "" above is a hack, but produce nicer code than "(,)"

Mapping sumbool to bool and sumor to option is not always nicer, but it helps when realizing stuff like lt_eq_lt_dec

Extract Inductive sumbool => Bool [ True False ].

Restore lazyness of andb, orb. NB: without these Extract Constant, andb/orb would be inlined by extraction in order to have lazyness, producing inelegant (if ... then ... else false) and (if ... then true else ...).

Extract Inductive nat => Int [ "0" "succ" ]
"(\ fO fS n -> if n==0 then (fO __) else fS (n-1))".

Efficient (but uncertified) versions for usual nat functions

Extract Constant pred => "\ n -> max 0 (n-1)".
Extract Inlined Constant max => max.

Extract Inlined Constant Peano_dec.eq_nat_dec => "(==)".

Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)".

Extraction "checker" Generate_and_Prune.