summaryrefslogtreecommitdiff
path: root/compiler/Pure.ml
diff options
context:
space:
mode:
authorSon HO2024-06-18 08:33:09 +0200
committerGitHub2024-06-18 08:33:09 +0200
commit43a9fb0fa5a1c03a7cce575a052f0d4201189d1d (patch)
treec967637249ea1c9001983e09e1f04f17b8e0a1d4 /compiler/Pure.ml
parent76ab141814644a94bffc8497e5845436d86b1083 (diff)
parent878be6d051f2f920fdc6c90add8423fa6f489492 (diff)
Merge pull request #246 from AeneasVerif/son/cleanup
Do some cleanup in the test files and the Lean backend
Diffstat (limited to '')
-rw-r--r--compiler/Pure.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index d07b8cfa..f7445575 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1077,11 +1077,18 @@ type fun_body = {
type item_kind = A.item_kind [@@deriving show]
+(** Attributes to add to the generated code *)
+type backend_attributes = {
+ reducible : bool; (** Lean "reducible" attribute *)
+}
+[@@deriving show]
+
type fun_decl = {
def_id : FunDeclId.id;
is_local : bool;
span : span;
kind : item_kind;
+ backend_attributes : backend_attributes;
num_loops : int;
(** The number of loops in the parent forward function (basically the number
of loops appearing in the original Rust functions, unless some loops are