-
Jakob Botsch Nielsen authored
This moves ChainStep and ChainTrace to type. The reason being that our proofs will depend on prefixes of traces and it will be very useful (if not required) to be able to match on the trace and the steps. ChainBuilderType is changed appropriately: now, an implementation just needs to prove that ChainTrace empty_env [] cur_env [] is inhabited. Thus, ChainTrace can basically be seen as one particular way to order the execution so that we reach a state. When it is inhabited, it thus means that there exists a proper way to order actions so that we reach the state we are in.
5221931a