diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-13 15:55:58 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-13 15:55:58 -0400 |
| commit | 7ae1f1d66c5d0cc5b7236162c7a14698a2c0e6c2 (patch) | |
| tree | 4effd0847db1b58cfb66cdb01e1e7c0d62941abd /src/Compilers/Named/ContextDefinitions.v | |
| parent | e860b3d92634bfb11d54b96effc05cb2aa9dba41 (diff) | |
Add lookupb_removeb_same
Diffstat (limited to 'src/Compilers/Named/ContextDefinitions.v')
| -rw-r--r-- | src/Compilers/Named/ContextDefinitions.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/Compilers/Named/ContextDefinitions.v b/src/Compilers/Named/ContextDefinitions.v index 386a1a363..f1a9b2741 100644 --- a/src/Compilers/Named/ContextDefinitions.v +++ b/src/Compilers/Named/ContextDefinitions.v @@ -48,12 +48,14 @@ Section with_context. : forall (ctx : Context) n t v, lookupb (extendb ctx n (t:=t) v) n t = Some v; lookupb_extendb_different : forall (ctx : Context) n n' t t' v, n <> n' -> lookupb (extendb ctx n (t:=t) v) n' t' - = lookupb ctx n' t'; + = lookupb ctx n' t'; lookupb_extendb_wrong_type : forall (ctx : Context) n t t' v, t <> t' -> lookupb (extendb ctx n (t:=t) v) n t' = None; - lookupb_removeb + lookupb_removeb_different : forall (ctx : Context) n n' t t', n <> n' -> lookupb (removeb ctx n t) n' t' - = lookupb ctx n' t'; + = lookupb ctx n' t'; + lookupb_removeb_same + : forall (ctx : Context) n t t', lookupb (removeb ctx n t) n t' = None; lookupb_empty : forall n t, lookupb (@empty _ _ _ Context) n t = None }. End with_context. |