diff options
| author | Brian Campbell | 2018-07-12 13:20:41 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-12 13:20:41 +0100 |
| commit | d3c75495194f810a89d10fede3ea377074af6f53 (patch) | |
| tree | 70ba08690e951f5dd35af458a3f0337753432638 /lib/coq/Sail2_prompt.v | |
| parent | fb33182ec89cfc4307ce5f04aa5e46d1c3c2716d (diff) | |
Coq: remove unnecessary constraint on foreach loops
Diffstat (limited to 'lib/coq/Sail2_prompt.v')
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 6448e81b..c98e2926 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -30,7 +30,7 @@ match l with foreachM xs vars body end. -Fixpoint foreach_ZM_up' {rv e Vars} from to step off n `{ArithFact (from <= to)} `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e := +Fixpoint foreach_ZM_up' {rv e Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e := if sumbool_of_bool (from + off <=? to) then match n with | O => returnm vars @@ -38,7 +38,7 @@ Fixpoint foreach_ZM_up' {rv e Vars} from to step off n `{ArithFact (from <= to)} end else returnm vars. -Fixpoint foreach_ZM_down' {rv e Vars} from to step off n `{ArithFact (to <= from)} `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e := +Fixpoint foreach_ZM_down' {rv e Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e := if sumbool_of_bool (to <=? from + off) then match n with | O => returnm vars @@ -46,9 +46,9 @@ Fixpoint foreach_ZM_down' {rv e Vars} from to step off n `{ArithFact (to <= from end else returnm vars. -Definition foreach_ZM_up {rv e Vars} from to step vars body `{ArithFact (from <= to)} `{ArithFact (0 < step)} := +Definition foreach_ZM_up {rv e Vars} from to step vars body `{ArithFact (0 < step)} := foreach_ZM_up' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. -Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (to <= from)} `{ArithFact (0 < step)} := +Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 < step)} := foreach_ZM_down' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. (*declare {isabelle} termination_argument foreachM = automatic*) |