diff options
| author | Brian Campbell | 2018-09-06 12:01:37 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-09-06 17:57:23 +0100 |
| commit | 387f0b0105992cc8c937424cdc411a46c7b3c979 (patch) | |
| tree | 9dacc5203204a26ffd31e9fff217e36b5b16bf02 /lib/coq/Sail2_prompt.v | |
| parent | caf395fe06b7d4205dad64f7962b60e5f77c02d8 (diff) | |
Coq: fill in a few more RISC-V axioms
Diffstat (limited to 'lib/coq/Sail2_prompt.v')
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 12c1a9d9..a0ef467e 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -127,6 +127,3 @@ Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad r Definition derive_m {rv e} {P Q:Z -> Prop} (x : monad rv {x : Z & P x} e) `{forall x, ArithFact (P x) -> ArithFact (Q x)} : monad rv {x : Z & (ArithFact (Q x))} e := x >>= fun y => returnm (build_ex (projT1 y)). - -Definition memea {rv e} {T:Type} (_:T) (_:Z) : monad rv unit e := returnm tt. -Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt. |