diff options
| author |  mark <> | 2012-02-23 11:00:45 +0000 |
|---|---|---|
| committer | mark <> | 2012-02-23 11:00:45 +0000 |
| commit | 448583e76767da575c9d90f54266d434c86282ed (patch) | |
| tree | f62d7cbd6b00c9d894929d37ff261efbd7b11916 /hol-light/TacticRecording/lib.ml | |
| parent | 6ecd3be998c4d2a6d8dae8ec2f67c50305a251ef (diff) | |
Capability for exporting .dot files added.
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 = |