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.16.1.tar.gz

sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

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

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

Sourceexception InternalDependencies

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