Why would Coq want to extract the specific Inductive definition to a specific OCaml type before extraction, isn’t that redundant?
Related topics
| Topic | Replies | Views | Activity | |
|---|---|---|---|---|
| Can I extract part of a module instead of the whole module? | 0 | 573 | January 20, 2021 | |
| PhD Position on Certified Extraction in Nantes | 0 | 1215 | September 8, 2020 | |
| Verified Extraction for Coq 8.19 | 0 | 136 | July 23, 2024 | |
| Best way to express that a type is inhabited in a way that allows getting the habitant | 1 | 571 | September 13, 2022 | |
| Inserting PPX annotations into extracted OCaml | 2 | 818 | October 12, 2020 |