1 files changed, 26 insertions, 0 deletions
diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig
index 51a09b9c..df879b4b 100644
--- a/backends/hol4/divDefLib.sig
+++ b/backends/hol4/divDefLib.sig
@@ -9,6 +9,32 @@
    divDefExampleTheory.
 
    For examples of how to use DefiveDiv, see divDefLibExampleScript.
+
+   Limitations: our encoding has limitations with regards to higher-order functions. More
+   precisely, the following definition wouldn't be accepted, because we don't know how
+   “MAP” would use ‘explore_tree’, meaning we can't prove the validity property required
+   by the fixed point upon defining ‘explore_tree’ and ‘explore_node’:
+
+   {[
+     Datatype tree:
+     | Leaf : int
+     | Node : tree list
+
+     explore_tree (t : tree) : tree =
+       case t of
+         Leaf i => Leaf i
+       | Node ns => Node (explore_node ns)
+
+     explore_node (ns : tree list) : tree list =
+       MAP explore_tree ns (* This is not supported *)
+   ]}
+
+   *However*, our encoding does allow defining a function ‘f’ *then* giving it
+   as argument to a higher-order function such as ‘MAP’.
+
+   Remark: "Partial recursive functions in higher-order logic", Alexander Krauss,
+   introduces an interesting approach by means of an inductive. It could be
+   interesting to try and compare.
  *)
 
 signature divDefLib =