1 files changed, 0 insertions, 27 deletions
diff --git a/xacml-proofs/lean/Xacml.lean.bak b/xacml-proofs/lean/Xacml.lean.bak
deleted file mode 100644
index bec63e6..0000000
--- a/xacml-proofs/lean/Xacml.lean.bak
+++ /dev/null
@@ -1,27 +0,0 @@
-inductive V₃ where
-  | true          : V₃
-  | false         : V₃
-  | indeterminate : V₃
-
-inductive V₆ where
-  | true_deny : V₆
-  | true_permit : V₆
-  | indeterminate_deny : V₆
-  | indeterminate_permit : V₆
-  | indeterminate : V₆
-  | false : V₆
-
-inductive Decision where
-  | permit : Decision
-  | deny   : Decision
-deriving Repr
-
--- structure Result where
---   decision    : Decision
---   obligations : Option (List String)
---   advice      : Option (List String)
--- deriving Repr
-
-def Result (α : Type) : Type := Decision × α
-
-#check ((Decision.permit, "Hi!") : Result String)