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.
Currently
payloadLang$configcontains a fieldletModule, and the assumption made forpayload_to_cakemlis that all functions used inLetbindings live in a module with nameletModule.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_cakemlphase and the associated proofs to allow the letfuns to live in different modules.