rename-everything

1 files changed, 16 insertions, 0 deletions

diff --git a/src/Compilers/Named/ContextOn.v b/src/Compilers/Named/ContextOn.v
new file mode 100644
index 000000000..6c06d3fbe
--- /dev/null
+++ b/src/Compilers/Named/ContextOn.v
@@ -0,0 +1,16 @@
+(** * Transfer [Context] across an injection *)
+Require Import Crypto.Compilers.Named.Syntax.
+
+Section language.
+  Context {base_type_code Name1 Name2 : Type}
+          (f : Name2 -> Name1)
+          (f_inj : forall x y, f x = f y -> x = y)
+          {var : base_type_code -> Type}.
+
+  Definition ContextOn (Ctx : Context Name1 var) : Context Name2 var
+    := {| ContextT := Ctx;
+          lookupb ctx n t := lookupb ctx (f n) t;
+          extendb ctx n t v := extendb ctx (f n) v;
+          removeb ctx n t := removeb ctx (f n) t;
+          empty := empty |}.
+End language.