package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.15.1.tar.gz

sha256=513e953b7183d478acb75fd6e80e4dc32ac1a918cf4343ac31a859cfb4e9aad2

doc/coq-core.vernac/Auto_ind_decl/index.html

Module `Auto_ind_decl`Source

This file is about the automatic generation of schemes about decidable equality,

author Vincent Siles

Oct 2007

Build boolean equality of a block of mutual inductive types

Sourceexception EqNotFound of Names.inductive * Names.inductive

Sourceexception EqUnknown of string

Sourceexception UndefinedCst of string

Sourceexception InductiveWithProduct

Sourceexception InductiveWithSort

Sourceexception ParameterWithoutEquality of Names.GlobRef.t

Sourceexception NonSingletonProp of Names.inductive

Sourceexception DecidabilityMutualNotSupported

Sourceexception NoDecidabilityCoInductive

Sourceexception ConstructorWithNonParametricInductiveType of Names.inductive

Sourceexception DecidabilityIndicesNotSupported

Sourceval beq_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

Build equivalence between boolean equality and Leibniz equality

Sourceval lb_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

Sourceval bl_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

Build decidability of equality

Sourceval eq_dec_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

On This Page

Build boolean equality of a block of mutual inductive types
Build equivalence between boolean equality and Leibniz equality
Build decidability of equality