diff options
| author | Brian Campbell | 2018-08-16 17:32:32 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-16 17:32:42 +0100 |
| commit | 18900d3c0da37c4dc7079749f84517fb7456e551 (patch) | |
| tree | 08e373e6b2bf301f36cdb302a01f4bad942f1166 /mips/mips_extras.v | |
| parent | eee4d26e53a5e33cdb71e9a338154e2dbf18830c (diff) | |
Add the type an expression was checked against to tannots, and use for Coq
Tweak extra Coq files to match.
Tweak early return rewrite to use declared return type, which can always
be put into an E_cast.
Diffstat (limited to 'mips/mips_extras.v')
| -rw-r--r-- | mips/mips_extras.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/mips/mips_extras.v b/mips/mips_extras.v index 626b4109..51856d9e 100644 --- a/mips/mips_extras.v +++ b/mips/mips_extras.v @@ -162,10 +162,12 @@ Require DecimalString. Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). -Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * size ÷ 8). +Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * (8 * size ÷ 8) ÷ 8). intros. rewrite Z.mul_comm. rewrite Z.quot_mul; auto with zarith. +rewrite Z.mul_comm with (m := size). +rewrite Z.quot_mul; auto with zarith. Qed. Hint Resolve MEMr_wrapper_lemma : sail. |