(** Extraction to Haskell : use of basic Haskell types *) Require Coq.extraction.Extraction. Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. Extract Inductive unit => "()" [ "()" ]. Extract Inductive list => "([])" [ "([])" "(:)" ]. Extract Inductive prod => "(,)" [ "(,)" ]. Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. Extract Inductive sumor => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ]. Extract Inlined Constant andb => "(Prelude.&&)". Extract Inlined Constant orb => "(Prelude.||)". Extract Inlined Constant negb => "Prelude.not".