diff options
Diffstat (limited to 'hol-light/TacticRecording/lib.ml')
| -rw-r--r-- | hol-light/TacticRecording/lib.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/hol-light/TacticRecording/lib.ml b/hol-light/TacticRecording/lib.ml index ae66892e..b1309f84 100644 --- a/hol-light/TacticRecording/lib.ml +++ b/hol-light/TacticRecording/lib.ml @@ -4,6 +4,13 @@ let rec copy n x = else [];; +let rec enumerate0 n xs = + match xs with + [] -> [] + | x::xs0 -> (n,x)::enumerate0 (n+1) xs0;; +let enumerate xs = enumerate0 1 xs;; + + (* foldr : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b *) let rec foldr f xs a = |