From 4598e77a9406d8040357c943a05dd1ab939932db Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Thu, 27 Jun 2024 01:56:05 +0200
Subject: Tidy up project

* Write README.md
* Add LICENSE
* Clean up some theorems and proofs
---
 expr.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'expr.v')

diff --git a/expr.v b/expr.v
index 11c0737..e770345 100644
--- a/expr.v
+++ b/expr.v
@@ -60,6 +60,12 @@ Instance Maybe_X_Attrset : Maybe X_Attrset := λ e,
   | _ => None
   end.
 
+Instance Maybe_X_V : Maybe X_V := λ e,
+  match e with
+  | X_V v => Some v
+  | _ => None
+  end.
+
 Instance Maybe_B_Nonrec : Maybe B_Nonrec := λ rhs,
   match rhs with
   | B_Nonrec e => Some e
-- 
cgit v1.2.3