X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=cc9c9aa6274fffe314ac3ef942417f95873ae5e0;hp=9b3a16378fb9e17371bccd95a3c5684715444113;hb=db8c9d54c285980e162e393efd1b7316887e5b80;hpb=9241d797587022ecd51e3c38cd34588de6745524

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 9b3a163..cc9c9aa 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -9,6 +9,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 
@@ -45,52 +46,6 @@ Set Printing Width 130.
  *)
 Section HaskFlattener.
 
-  Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) : HaskLevel Γ :=
-    match lht with t @@ l => l end.
-
-  Definition arrange :
-    forall {T} (Σ:Tree ??T) (f:T -> bool),
-      Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
-    intros.
-    induction Σ.
-      simpl.
-      destruct a.
-      simpl.
-      destruct (f t); simpl.
-      apply RuCanL.
-      apply RuCanR.
-      simpl.
-      apply RuCanL.
-      simpl in *.
-      eapply RComp; [ idtac | apply arrangeSwapMiddle ].
-      eapply RComp.
-      eapply RLeft.
-      apply IHΣ2.
-      eapply RRight.
-      apply IHΣ1.
-      Defined.
-
-  Definition arrange' :
-    forall {T} (Σ:Tree ??T) (f:T -> bool),
-      Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
-    intros.
-    induction Σ.
-      simpl.
-      destruct a.
-      simpl.
-      destruct (f t); simpl.
-      apply RCanL.
-      apply RCanR.
-      simpl.
-      apply RCanL.
-      simpl in *.
-      eapply RComp; [ apply arrangeSwapMiddle | idtac ].
-      eapply RComp.
-      eapply RLeft.
-      apply IHΣ2.
-      eapply RRight.
-      apply IHΣ1.
-      Defined.
 
   Ltac eqd_dec_refl' :=
     match goal with