Controlling Extraction of Specific Types

liuxingpeng520521 September 4, 2023, 5:48am 1

Why would Coq want to extract the specific Inductive definition to a specific OCaml type before extraction, isn’t that redundant?

Topic		Replies	Views
Can I extract part of a module instead of the whole module? Using Coq	0	566	January 20, 2021
Extraction to Haskell Int type Using Coq	2	698	July 26, 2021
Verified Extraction for Coq 8.19 Announcements	0	96	July 23, 2024
Generating depth-indexed variant of an inductive Using Coq	1	329	June 16, 2023
Ocaml native int63 extraction Using Coq	0	375	October 3, 2023