+(*********************************************************************************************************************************)
+(* Extraction: *)
+(* *)
+(* This module is the "top level" for extraction *)
+(* *)
+(*********************************************************************************************************************************)
+
(* need this or the Haskell extraction fails *)
Set Printing Width 1300000.
Require Import HaskCoreToWeak.
Require Import HaskWeakToStrong.
Require Import HaskStrongToProof.
-Require Import HaskProofToStrong.
Require Import HaskProofToLatex.
Require Import HaskStrongToWeak.
Require Import HaskWeakToCore.
+Require Import HaskProofToStrong.
+
+Require Import HaskProofCategory.
+Require Import HaskStrongCategory.
+Require Import ReificationsEquivalentToGeneralizedArrows.
Open Scope string_scope.
Extraction Language Haskell.
(*
Definition TInt : HaskType nil ★.
assert (tyConKind' intPrimTyCon = ★).
- admit.
rewrite <- H.
unfold HaskType; intros.
apply TCon.