lthms/FreeSpec

Should we restrict the domain of [abstract_step] to valid effects and results?

vtourneur opened this issue · 1 comments

vtourneur commented
Should we restrict the domain of [abstract_step] to valid effects and results?
lthms commented

As of now, we cannot do that easily, since it would mean we always have a proof of requirements when calling witness_update.