Letfuns shouldn't have to live in the same module
Open
enhancement
good first issue
- Dominant language
- Standard ML
- Stars
- 2
- Forks
- 4
- PR merge metrics
- No merged PRs in 30d
Description
Currently `payloadLang$config` contains a field `letModule`, and the assumption made for `payload_to_cakeml` is that all functions used in `Let` bindings live in a module with name `letModule`.
This seems overly restrictive: for example, it would be convenient to be able to supply some functions as part of a standard library.
This issue is to adapt the `payload_cakeml` phase and the associated proofs to allow the letfuns to live in different modules.
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.