blob: 4c02e26c72e0e82f43aed8d11cea9d976271073e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
(** * Transfer [Context] across an injection *)
Require Import Crypto.Compilers.Named.Context.
Require Import Crypto.Compilers.Named.ContextDefinitions.
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 |}.
Lemma ContextOnOk {Ctx} (COk : ContextOk Ctx) : ContextOk (ContextOn Ctx).
Proof.
split; intros; try apply COk; auto.
Qed.
End language.
Arguments ContextOnOk {_ _ _ f} f_inj {_ _} COk.
|
