A verified Candle compute primitive.
computeProofScript.sml: Proof of correctness for the compute primitive.
computeScript.sml: Implementation of the compute primitive.
compute_evalProofScript.sml: Proofs about the interpreter function for the Candle compute primitive.
compute_evalScript.sml: Interpreter function for the Candle compute primitive.
compute_execProofScript.sml: Verification of fast interpreter for the Candle compute primitive.
compute_execScript.sml: Fast interpreter function for the Candle compute primitive.
compute_pmatchScript.sml: Pmatch definitions for functions in computeScript.sml.
compute_syntaxProofScript.sml: Proofs related to term embeddings for the Candle compute primitive.
compute_syntaxScript.sml: Definitions of 'compute expressions' for the Candle compute primitive.