X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=08485a1307f781e3923c00b53c4c302190dcd45a;hp=308e6692895a7b36b1a3f634d1e3528c067f3311;hb=a9a60dc234f76a4740b32c0f62aa0fe3a89fea83;hpb=257c3cfd16b2f49778559b76404c629e9b335362

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 308e669..08485a1 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -1220,8 +1220,29 @@ Section HaskFlattener.
 
     destruct case_RLetRec.
       rename t into lev.
+      simpl. destruct lev; simpl.
+      replace (getjlev (y @@@ nil)) with (nil: (HaskLevel Γ)).
+      replace (mapOptionTree flatten_leveled_type (y @@@ nil))
+        with  ((mapOptionTree flatten_type y) @@@ nil).
+      unfold flatten_leveled_type at 2.
       simpl.
-      apply (Prelude_error "LetRec not supported (FIXME)").
+      unfold flatten_leveled_type at 3.
+      simpl.
+      apply nd_rule.
+      set (@RLetRec Γ Δ (mapOptionTree flatten_leveled_type lri) (flatten_type x) (mapOptionTree flatten_type y) nil) as q.
+      simpl in q.
+      apply q.
+        induction y; try destruct a; auto.
+        simpl.
+        rewrite IHy1.
+        rewrite IHy2.
+        reflexivity.
+        induction y; try destruct a; auto.
+        simpl.
+        rewrite <- IHy1.
+        rewrite <- IHy2.
+        reflexivity.
+      apply (Prelude_error "LetRec not supported inside brackets yet (FIXME)").
 
     destruct case_RCase.
       simpl.