diff options
| -rw-r--r-- | backends/hol4/divDefLib.sig | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig index 0de88db5..ac9c6892 100644 --- a/backends/hol4/divDefLib.sig +++ b/backends/hol4/divDefLib.sig @@ -16,9 +16,11 @@ by the fixed point upon defining ‘explore_tree’ and ‘explore_node’: {[ - Datatype tree: - | Leaf : int - | Node : tree list + Datatype: + tree = + Leaf int + | Node (tree list) + End explore_tree (t : tree) : tree = case t of |