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

sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

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