This repository was archived by the owner on Mar 7, 2024. It is now read-only.
This repository was archived by the owner on Mar 7, 2024. It is now read-only.
Open
Description
A Rust variant of arity n is extracted as an F* constructor of arity one whose payload is a tuple of size n.
For instance, the Rust code bellow:
enum Foo {
CaseX(u16),
CaseY(u8, u8),
}
struct Bar(u8, u8);is translated as the following F*:
noeq type foo_t =
| CaseX_foo_t : pub_uint16-> foo_t
| CaseY_foo_t : (pub_uint8 & pub_uint8) -> foo_t
noeq type bar_t =
| Bar_bar_t : (pub_uint8 & pub_uint8) -> bar_tThis is not very idiomatic in F*, and disallows using F* projectors (e.g. (Bar_bar_t 4 8)._1).
In the context of PR #323, having F* projectors would simplify a lot extraction.
Metadata
Metadata
Assignees
Labels
No labels