add partial support for flattening kappa-expressions (mostly commented out)

[coq-hetmet.git] / src / HaskWeak.v

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 077f7b5..9d39f44 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -31,6 +31,10 @@ Inductive WeakExpr :=
 | WETyApp     : WeakExpr                        -> WeakType                  -> WeakExpr
 | WECoApp     : WeakExpr                        -> WeakCoercion              -> WeakExpr
 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
+(*
+| WEKappa     : WeakExprVar                     -> WeakExpr                  -> WeakExpr
+| WEKappaApp  : WeakExpr                        -> WeakExpr                  -> WeakExpr
+*)
 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr