diff options
| author |  Unknown <aleks@aleks-PC.hsd1.ma.comcast.net.> | 2012-02-06 23:54:17 -0500 |
|---|---|---|
| committer | Unknown <aleks@aleks-PC.hsd1.ma.comcast.net.> | 2012-02-06 23:54:17 -0500 |
| commit | 20bab8ed995ac952ca6bea347786d2c2cdceb1c6 (patch) | |
| tree | dcd86a81675184178becb3edbdb1cd70b2db9c43 /Jennisys/Utils.fs | |
| parent | 4888eb23bb6ccd0900915ee00d9fcbc25c2f21e1 (diff) | |
Jennisys: (1) fixed Jennisys to work with the latest version of Dafny/Boogie
(translation from Dafny to Boogie seems to have changed, so Jennisys was
having trouble reading back Dafny models); (2) added a doubly-linked list
example
Diffstat (limited to 'Jennisys/Utils.fs')
| -rw-r--r-- | Jennisys/Utils.fs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs index 469e5e5a..56b6b779 100644 --- a/Jennisys/Utils.fs +++ b/Jennisys/Utils.fs @@ -207,11 +207,11 @@ let ListContains elem lst = let ListRemove elem lst =
lst |> List.choose (fun e -> if e = elem then None else Some(e))
-let rec ListRemoveNth n lst =
- if n = 0 then
+let rec ListRemoveIdx idx lst =
+ if idx = 0 then
List.tail lst
- else
- List.head lst :: ListRemoveNth (n-1) (List.tail lst)
+ else
+ List.head lst :: ListRemoveIdx (idx - 1) (List.tail lst)
// ===============================================================
/// ensures: |ret| = max(|lst| - cnt, 0)
|