A module for the inductive theorem prover Coq, which generates function and theorems based on inductive type definitions.
Compatible with Coq 8.4
A module for the inductive theorem prover Coq, which generates function and theorems based on inductive type definitions.
Compatible with Coq 8.4