help wanted
Métriques du dépôt
- Stars
- (1 169 étoiles)
- Métriques de merge PR
- (Métriques PR en attente)
Description
Currently the CakeML tutorial, i.e. the files under tutorial/solutions and particularly wordfreqProgScript.sml, is based on CF proofs.
Since the monadic translator, which is described in Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions, could produce the same program in a nicer way, I think the tutorial should be ported to use the monadic translator.
One can take inspiration from existing examples that use the monadic translator.