We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
effect
1 parent 03bf5cd commit 6e60ce5Copy full SHA for 6e60ce5
engine/backends/fstar/fstar_backend.ml
@@ -950,14 +950,14 @@ struct
950
match args with
951
| [] -> typ
952
| _ ->
953
- let mk namespace effect = F.term_of_lid (namespace @ [ effect ]) in
+ let mk namespace eff = F.term_of_lid (namespace @ [ eff ]) in
954
let prims = mk [ "Prims" ] in
955
- let effect =
+ let eff =
956
if Option.is_some prepost_bundle then
957
if is_lemma then mk [] "Lemma" else prims "Pure"
958
else prims "Tot"
959
in
960
- F.mk_e_app effect (if is_lemma then List.drop args 1 else typ :: args)
+ F.mk_e_app eff (if is_lemma then List.drop args 1 else typ :: args)
961
962
(** Prints doc comments out of a list of attributes *)
963
let pdoc_comments attrs =
0 commit comments