Comment on extract_as being recursive.

FStarLang · Sep 26, 2024 · b887b0f · b887b0f
1 parent 1ee7ce5
commit b887b0f
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/src/extraction/FStar.Extraction.ML.Modul.fst b/src/extraction/FStar.Extraction.ML.Modul.fst
@@ -756,6 +756,8 @@ let mark_sigelt_erased (se:sigelt) (g:uenv) : uenv =
 let fixup_sigelt_extract_as se =
   match se.sigel, find_map se.sigattrs N.is_extract_as_attr with
   | Sig_let {lids; lbs=(_, [lb])}, Some impl ->
+    // The specified implementation can be recursive,
+    // to be on the safe side we always mark the replaced sigelt as recursive.
     {se with sigel = Sig_let {lids; lbs=(true, [{lb with lbdef = impl}])}}
   | _ -> se
 

diff --git a/ulib/FStar.ExtractAs.fst b/ulib/FStar.ExtractAs.fst
@@ -31,5 +31,7 @@ open FStar.Stubs.Reflection.Types
     and most likely cause the extracted program to crash.
 
     Note that the argument needs to be a literal quotation.
+    The implementation can be recursive,
+    but then you need to construct the attribute via a tactic.
  *)
 let extract_as (impl: term) = ()