Merge pull request #1355 from cryspen/fix-lemmas-fstar-backend

fix(engine/fstar-backend): drop spurious precondition on `Lemma`s

Author: W95Psp

engine/backends/fstar/fstar_backend.ml

@@ -943,7 +943,7 @@ struct
             if is_lemma then mk [] "Lemma" else prims "Pure"
           else prims "Tot"
         in
-        F.mk_e_app effect (if is_lemma then args else typ :: args)
+        F.mk_e_app effect (if is_lemma then List.drop args 1 else typ :: args)
 
   (** Prints doc comments out of a list of attributes *)
   let pdoc_comments attrs =

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -565,10 +565,10 @@ let issue_844_ (e_x: u8)
           true) = e_x
 
 let add3_lemma (x: u32)
-    : Lemma Prims.l_True
-      (ensures
-        x <=. mk_u32 10 || x >=. (u32_max /! mk_u32 3 <: u32) ||
-        (add3 x x x <: u32) =. (x *! mk_u32 3 <: u32)) = ()
+    : Lemma
+    (ensures
+      x <=. mk_u32 10 || x >=. (u32_max /! mk_u32 3 <: u32) ||
+      (add3 x x x <: u32) =. (x *! mk_u32 3 <: u32)) = ()
 
 type t_Foo = {
   f_x:u32;