This adds evaluation of primitive terms to all the evaluation relations and proves correctness of erasure and all the compilation phases, i.e. they preserve evaluation of primitives. We still do not give semantics to primitive operations though, only explicit values are handled. An array is evaluated when its default value and list of values are evaluated, cbv-style.
This adds evaluation of primitive terms to all the evaluation relations and proves correctness of erasure and all the compilation phases, i.e. they preserve evaluation of primitives. We still do not give semantics to primitive operations though, only explicit values are handled. An array is evaluated when its default value and list of values are evaluated, cbv-style.