Skip to content
  • Jakob Botsch Nielsen's avatar
    Move ChainStep and ChainTrace to Type · 5221931a
    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