diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-06-05 22:42:28 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-06-05 22:42:28 +0100 |
commit | 48d907ee56b39e7a8819700ae8a88af05c1b031e (patch) | |
tree | 0d9cddc5622e5b9953b871908195aa606b3dd748 /src/hls/Gible.v | |
parent | 2e731050c69c98142d29d87fb863f199d50dfe19 (diff) | |
download | vericert-48d907ee56b39e7a8819700ae8a88af05c1b031e.tar.gz vericert-48d907ee56b39e7a8819700ae8a88af05c1b031e.zip |
Fix many more lemmas
Diffstat (limited to 'src/hls/Gible.v')
-rw-r--r-- | src/hls/Gible.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/hls/Gible.v b/src/hls/Gible.v index e50fdc0..c51b250 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -613,4 +613,14 @@ type ~genv~ which was declared earlier. end ) b nil. + Definition pred_uses i := + match i with + | RBop (Some p) _ _ _ + | RBload (Some p) _ _ _ _ + | RBstore (Some p) _ _ _ _ + | RBexit (Some p) _ => predicate_use p + | RBsetpred (Some p) _ _ p' => p' :: predicate_use p + | _ => nil + end. + End Gible. |