diff options
| author | Brian Campbell | 2019-12-19 18:04:55 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-12-19 18:41:20 +0000 |
| commit | 866d8e5e2d7da11b0c34800679dbdc2d5d8fd8f2 (patch) | |
| tree | 1eb7dcebe8579de2f221e0f99e7ed32911e6e577 /x86/x86_extras_embed_sequential.lem | |
| parent | 1aeb3db72e08a463e04632992ca3bd668ee4e52e (diff) | |
Coq library improvements
- add liftRS support to tactics
- define uint and sint in terms of functions without proof terms
- eq_vec correctness
- lemma that rounding up integers using reals is the obvious integer calculation
- another proof irrelevance tactic
- try lemmas in the sail hintdb both before and after goal processing
Diffstat (limited to 'x86/x86_extras_embed_sequential.lem')
0 files changed, 0 insertions, 0 deletions