search

runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.
Other
17 stars 6 forks source link

Create dexter-properties.md #245

Closed daejunpark closed 3 years ago

ehildenb commented 3 years ago

It may make sense to integrate some of the properties directly into dexter.md or dexter-spec.md. Take a look and see if it makes sense, otherwise it's fine where it is.

hjorthjort commented 3 years ago

I agree that it's probably better to inline this in dexter and dexter-spec. But the invariants and descriptions look good to me.