diff options
| author | Son Ho | 2023-05-15 16:48:52 +0200 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | b1dd8274d7a1cff2b9427e4356b66c4e63fe498c (patch) | |
| tree | a7cd54579232ba3ebe1895340cac26cc29b9efc9 | |
| parent | 74e8e6b80b31b1df9123fbec9a7f910a68a0b1cd (diff) | |
Make a minor modification
Diffstat (limited to '')
| -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 |