diff --git a/cedar-lean/Cedar/Spec/EntitySlice.lean b/cedar-lean/Cedar/Spec/EntitySlice.lean
new file mode 100644
index 000000000..e69de29bb
diff --git a/cedar-lean/Cedar/Spec/Evaluator.lean b/cedar-lean/Cedar/Spec/Evaluator.lean
index eb6badf7e..9808762fc 100644
--- a/cedar-lean/Cedar/Spec/Evaluator.lean
+++ b/cedar-lean/Cedar/Spec/Evaluator.lean
@@ -118,3 +118,13 @@ def evaluate (x : Expr) (req : Request) (es : Entities) : Result Value :=
     call xfn vs
 
 end Cedar.Spec
+
+namespace Cedar.Spec.Monadic
+
+def Trap (m : Type  → Type ) (α : Type ) : Type  :=
+  m α → (Bool × α)
+
+
+
+
+end Cedar.Spec.Monadic