Session CakeML_Codegen

Theories

• ML_Utils
  • File ‹utils.ML›
• Compiler_Utils
• Code_Utils
  • File ‹pattern_compatibility.ML›
  • File ‹dynamic_unfold.ML›
• CakeML_Utils
• Test_Utils
• Doc_Terms
• Terms_Extras
  • File ‹hol_term.ML›
• HOL_Datatype
  • File ‹hol_datatype.ML›
• Constructors
• Consts
• Strong_Term
• Sterm
• Pterm
• Term_as_Value
• Value
• Doc_CupCake
• CupCake_Env
• CupCake_Semantics
• Doc_Rewriting
• General_Rewriting
• Rewriting_Term
• Rewriting_Nterm
• Rewriting_Pterm_Elim
• Rewriting_Pterm
• Rewriting_Sterm
• Big_Step_Sterm
• Big_Step_Value
• Big_Step_Value_ML
• Doc_Preproc
• Eval_Class
  • File ‹tactics.ML›
• Embed
  • File ‹embed.ML›
• Eval_Instances
  • File ‹eval_instances.ML›
• Doc_Backend
• CakeML_Setup
• CakeML_Backend
• CakeML_Correctness
• CakeML_Byte
• Doc_Compiler
• Composition
• Compiler
• Test_Composition
• Test_Print
• Test_Embed_Data
• Test_Embed_Data2
• Test_Embed_Tree
• Test_Datatypes