blob: 6c06d3fbedf70726215ca0ab402e5ffb48d385fb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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.
|
