Prove the paper's counts, levelization, depth bounds, recipe lengths and Section 6 in Rocq, and revise the paper
8397e00 | From Stdlib Require Import Extraction ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlZInt. | |
| From TH Require Import ExtrNat Net Phys. | |
| Extraction Language OCaml. | |
| Set Extraction Output Directory "extract". | |
| Extraction "physnet.ml" phys_units phys_next nst. | |