diff options
| -rw-r--r-- | lib/coq/Sail2_values.v | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index d1f6e560..0fdaa7aa 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1236,15 +1236,17 @@ end. (*declare {isabelle} termination_argument foreach = automatic val index_list : Z -> Z -> Z -> list Z*) -Fixpoint index_list' from step n := - match n with - | O => [] - | S n => from :: index_list' (from + step) step n - end. +Fixpoint index_list' from to step n := + if orb (andb (step >? 0) (from <=? to)) (andb (step <? 0) (to <=? from)) then + match n with + | O => [] + | S n => from :: index_list' (from + step) to step n + end + else []. Definition index_list from to step := if orb (andb (step >? 0) (from <=? to)) (andb (step <? 0) (to <=? from)) then - index_list' from step (S (Z.abs_nat (from - to))) + index_list' from to step (S (Z.abs_nat (from - to))) else []. (*val while : forall vars. vars -> (vars -> bool) -> (vars -> vars) -> vars |