Start working on function extraction

1 files changed, 10 insertions, 0 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index a1b56964..a839c0a3 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -469,3 +469,13 @@ let extract_fun_def_register_names (ctx : extraction_ctx)
   in
   (* Return *)
   ctx
+
+(** Extract a function definition.
+
+    Note that all the names used for extraction should already have been
+    registered.
+ *)
+let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
+    (qualif : fun_def_qualif) (def : fun_def) : unit =
+  (* TODO *)
+  ()