menu

Return to entry

ML_Utils
Compiler_Utils
Code_Utils
CakeML_Utils
Test_Utils
Doc_Terms
Terms_Extras
HOL_Datatype
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
Embed
Eval_Instances
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

CakeML_Codegen.Rewriting_Pterm_Elim

HTML Presentation