A few other examples of HOL functions that can be translated into CakeML.
auxiliary: This directory contains definitions used for miscellaneous translator examples from used in the original ICFP paper about the translator.
example_91Script.sml: This is a simple example of applying the translator to the 91 function.
example_balanced_bstScript.sml: This is a simple example of applying the translator to a balanced binary tree from HOL.
example_copying_gcScript.sml: This is a simple example of applying the translator to an algorithm-level model of a copying garbage collector.
example_parser_genScript.sml: This is a simple example of applying the translator to a parser generator.
example_primality_testScript.sml: This is a simple example of applying the translator to an efficient primaliy tester formalised by Joe Hurd.
example_qsortScript.sml: This is a simple example of applying the translator to a functional version of quick sort.
example_regexp_matcherScript.sml: This is a simple example of applying the translator to a matcher for regular expressions.