Skip to content

Draft : Working towards extraction

Germán Delbianco requested to merge germanD@pack-module-types into master

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

Merge request reports