diff options
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 8 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 8 |
2 files changed, 8 insertions, 8 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*) diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index d18b17bb..13352f4b 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1330,7 +1330,7 @@ Fixpoint foreach_Z' {Vars} from to step n (vars : Vars) (body : Z -> Vars -> Var Definition foreach_Z {Vars} from to step vars body := foreach_Z' (Vars := Vars) from to step (S (Z.abs_nat (from - to))) vars body. -Fixpoint foreach_Z_up' {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 -> Vars) {struct n} : Vars := +Fixpoint foreach_Z_up' {Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> Vars) {struct n} : Vars := if sumbool_of_bool (from + off <=? to) then match n with | O => vars @@ -1338,7 +1338,7 @@ Fixpoint foreach_Z_up' {Vars} from to step off n `{ArithFact (from <= to)} `{Ari end else vars. -Fixpoint foreach_Z_down' {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 -> Vars) {struct n} : Vars := +Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> Vars) {struct n} : Vars := if sumbool_of_bool (to <=? from + off) then match n with | O => vars @@ -1346,9 +1346,9 @@ Fixpoint foreach_Z_down' {Vars} from to step off n `{ArithFact (to <= from)} `{A end else vars. -Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (from <= to)} `{ArithFact (0 < step)} := +Definition foreach_Z_up {Vars} from to step vars body `{ArithFact (0 < step)} := foreach_Z_up' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. -Definition foreach_Z_down {Vars} from to step vars body `{ArithFact (to <= from)} `{ArithFact (0 < step)} := +Definition foreach_Z_down {Vars} from to step vars body `{ArithFact (0 < step)} := foreach_Z_down' (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. (*val while : forall vars. vars -> (vars -> bool) -> (vars -> vars) -> vars |