Draft : Working towards extraction
We want to extract the Coq model (and tests the PBT devs over them). We need to take several steps.
-
Pack commitments as Module types #9 (closed) -
Pack nats that should be uints as a ADT so we can choose to extract to them -
Domain tying to avoid overflows?
Edited by Germán Delbianco