HomeIsabelle/Phabricator

Generate the main part of a callback in the first application to the argument…

Description

Generate the main part of a callback in the first application to the argument and result types.
Applying it to a specific function then adds a small two-instruction stub.

Details

Provenance
dcjmAuthored on May 24 2019, 5:23 PM
Parents
rPOLYML07c9e32fcf82: Add original version of ForeignMemory for bootstrapping.
Branches
Unknown
Tags
Unknown