summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/hol4/divDefLib.sig8
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