|
|
|---|
|
|
|
|---|
Refinement of the state to a stobj.
We refine the type stat of states to a stobj straightforwardly derived from the definition of stat. This is not the most efficient refinement of the states, but it is a simple one to explore at the beginning; we will explore more complex and efficient stobjs later.
We introduce the stobj, and we define an isomorphism between the stobj type and the stat type. Then we refine the rest of the model to use the stobj representation; this is work in progress.