summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-05-15 16:48:52 +0200
committerSon HO2023-06-04 21:54:38 +0200
commitb1dd8274d7a1cff2b9427e4356b66c4e63fe498c (patch)
treea7cd54579232ba3ebe1895340cac26cc29b9efc9
parent74e8e6b80b31b1df9123fbec9a7f910a68a0b1cd (diff)
Make a minor modification
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