Add support for `FDIFF _ (FDOM _)` to translator - #1444

Open

myreen wants to merge 8 commits into

Commits on Aug 4, 2026

Add support for FDIFF _ (FDOM _) to HOL->CakeML translator
myreen
committed
5f5ccf3
Add mlstring$fast_compare and prove TotOrd_fast_compare

myreen
and
claude
committed
914eaf6

Commits on Aug 5, 2026

Set up bootstrap translation for better finite map translations
myreen
committed
815cf41
More work on finite maps and the translator
myreen
committed
2eee534
Changes missed in previous commit
myreen
committed
175554b

Commits on Aug 7, 2026

Fix inferProg for finite map change
myreen
committed
01d157a

Commits on Aug 10, 2026

Remove old fmap support in HOL->CakeML translator
myreen
committed
2aa89b6

Commits on Aug 12, 2026

Fix PEG translations
myreen
committed
5ccbdb6