Skip to content

Conversation

@Nadrieril
Copy link
Member

@Nadrieril Nadrieril commented Aug 28, 2024

Fixes #231. This also removes the BoxFree builtin that no longer exists in rustc, which fixes #230.

@Nadrieril Nadrieril merged commit 6b5e110 into AeneasVerif:main Aug 28, 2024
@Nadrieril Nadrieril deleted the rename-assumed-to-builtin branch August 28, 2024 13:01
(** An built-in function identifier, identifying a function coming from a
standard library.
*)
type assumed_fun_id =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this also be renamed to builtin_fun_id? :)

| Shl -> "<<"
| Shr -> ">>"

let assumed_fun_id_to_string (aid : assumed_fun_id) : string =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same comment

TODO: move to assumed.rs?
TODO: move to builtins.rs?
*)
type assumed_ty =
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same comment

and external ADTs).
*)
| TTuple
| TAssumed of assumed_ty
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same

@Nadrieril
Copy link
Member Author

Nadrieril commented Aug 29, 2024

@sonmarcho That was intentional, this PR is only for the rust side. I'll propagate to the OCaml side separately.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Rename assumed to builtin Check that box_free is still used

2 participants