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 Rocq	0	567	January 20, 2021
Extraction to Haskell Int type Using Rocq	2	700	July 26, 2021
Verified Extraction for Coq 8.19 Announcements	0	132	July 23, 2024
Generating depth-indexed variant of an inductive Using Rocq	1	329	June 16, 2023
Ocaml native int63 extraction Using Rocq	0	383	October 3, 2023