Skip to content

Commit

Permalink
Merge pull request #589 from hacspec/fix-trivial-let-rec-intf-fstar
Browse files Browse the repository at this point in the history
fix(engine/backend): F*: `rec` qual. when interface mode
  • Loading branch information
W95Psp authored Apr 9, 2024
2 parents 92300ad + c5db016 commit 00b125b
Showing 1 changed file with 3 additions and 4 deletions.
7 changes: 3 additions & 4 deletions engine/backends/fstar/fstar_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -802,9 +802,10 @@ struct
params
in
let pat = F.pat @@ F.AST.PatApp (pat, pat_args) in
let qualifier = F.AST.(if is_rec then Rec else NoLetQualifier) in
let impl =
F.decl ~fsti:false
@@ F.AST.TopLevelLet (NoLetQualifier, [ (pat, pexpr body) ])
@@ F.AST.TopLevelLet (qualifier, [ (pat, pexpr body) ])
in
let interface_mode = ctx.interface_mode && not (List.is_empty params) in
let ty =
Expand Down Expand Up @@ -836,9 +837,7 @@ struct
in
let pat = F.pat @@ F.AST.PatAscribed (pat, (ty, None)) in
let full =
F.decl
@@ F.AST.TopLevelLet
((if is_rec then Rec else NoLetQualifier), [ (pat, pexpr body) ])
F.decl @@ F.AST.TopLevelLet (qualifier, [ (pat, pexpr body) ])
in

let intf = F.decl ~fsti:true (F.AST.Val (name, arrow_typ)) in
Expand Down

0 comments on commit 00b125b

Please sign in to comment.