Changeset 2516 for src/ASM/AssemblyProof.ma

Timestamp:

Dec 2, 2012, 5:45:36 PM (7 years ago)

Author:

mckinna

Message:

removed typedefs; restored older versions; moved typedefs to compiler.ma
AssemblyProofSplit? *still* doesn't typecheck: disambiguation errors!

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -192 +192 @@
   ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
   ∀assembled.
-  ∀costs': costlabel_map.
+  ∀costs': BitVectorTrie costlabel 16.
   let 〈preamble, instr_list〉 ≝ program in
   let 〈labels, costs〉 ≝ create_label_cost_map instr_list in