diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-13 14:37:01 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-13 14:37:01 -0400 |
| commit | 9c101df02cffe6580cb84a9909b1c244831dcde9 (patch) | |
| tree | ca5a15fb4c5134b81c8fe48b4a3d2845fc5a9d55 /src/Compilers/Named | |
| parent | 673399a0aa43c94e5a3112164a6b373c61a2ae7a (diff) | |
Add ContextOnOk
Diffstat (limited to 'src/Compilers/Named')
| -rw-r--r-- | src/Compilers/Named/ContextOn.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Compilers/Named/ContextOn.v b/src/Compilers/Named/ContextOn.v index 5e51f7585..4c02e26c7 100644 --- a/src/Compilers/Named/ContextOn.v +++ b/src/Compilers/Named/ContextOn.v @@ -1,5 +1,6 @@ (** * 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} @@ -13,4 +14,11 @@ Section language. 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. |