diff options
Diffstat (limited to 'src/ExtractToFStar.ml')
| -rw-r--r-- | src/ExtractToFStar.ml | 10 |
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 *) + () |