Add function signature only in interface mode.

engine/backends/fstar/fstar_backend.ml

@@ -959,9 +959,11 @@ struct
 
         let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in
 
-        if is_erased then intf :: erased_impl name arrow_typ []
-        else if interface_mode then [ impl; intf ]
-        else [ full ]
+        let erased = erased_impl name arrow_typ [] in
+        let impl, full =
+          if is_erased then (erased, erased) else ([ impl ], [ full ])
+        in
+        if interface_mode then intf :: impl else full
     | TyAlias { name; generics; ty } ->
         let pat =
           F.pat

test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap

@@ -71,6 +71,4 @@ class t_T (v_Self: Type0) = {
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 val impl_T_for_u8:t_T u8
-
-val c:u8
 '''

test-harness/src/snapshots/toolchain__interface-only into-fstar.snap

@@ -38,14 +38,6 @@ open FStar.Mul
 /// modifier, `f` is still extractable as an interface.
 /// Expressions within type are still extracted, as well as pre- and
 /// post-conditions.
-val f (x: u8)
-    : Prims.Pure (t_Array u8 (sz 4))
-      (requires x <. 254uy)
-      (ensures
-        fun r ->
-          let r:t_Array u8 (sz 4) = r in
-          (r.[ sz 0 ] <: u8) >. x)
-
 assume
 val f': x: u8
   -> Prims.Pure (t_Array u8 (sz 4))
@@ -81,8 +73,6 @@ val impl_1': Core.Convert.t_From t_Bar u8
 
 let impl_1 = impl_1'
 
-val from__from: u8 -> t_Bar
-
 assume
 val from__from': u8 -> t_Bar