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

sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250

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