package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz

sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

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