package coq

You can search for identifiers within the package.

in-package search v0.2.0

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

package coq

coq-core.boot
- Boot
  - Env
    
    Path
  - Path
  - Usage
  - Util
coq-core.clib
- CArray
  - ExtS
    
    Floatarray
    
    Fun1
    
    Smart
    
    Smart
  - Floatarray
  - Fun1
    
    Smart
  - Smart
- CEphemeron
- CList
  - ExtS
    
    MonoS
    
    Smart
  - MonoS
  - Smart
- CMap
  - ExtS
    
    Monad
    
    M
    
    Set
    
    Smart
  - MonadS
  - OrderedType
- CObj
- CSet
  - Hashcons
    
    H
    
    M
  - HashedType
  - OrderedType
- CString
  - ExtS
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Pred
  - List
  - Map
    
    Monad
    
    M
    
    Smart
  - Pred
- CThread
- CUnix
- Diff2
  - Make
    
    M
  - S
  - SeqType
- Dyn
  - Make
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - MapS
  - S
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - ValueS
- Exninfo
- HMap
  - HashedType
  - Make
    
    M
    
    Monad
    
    M
    
    Set
    
    Smart
- Hashcons
  - HashconsedType
  - HashedType
  - Hlist
    
    D
  - Hstring
  - Make
    
    X
  - S
- Hashset
  - Combine
  - EqType
  - Make
    
    E
  - S
- Heap
  - Functional
    
    X
  - Ordered
  - S
- IStream
- Int
  - List
  - Map
    
    Monad
    
    M
    
    Smart
  - PArray
  - PMap
- Monad
  - Def
  - ListS
  - Make
    
    List
    
    M
  - S
    
    List
- NeList
- Option
  - List
  - Smart
- OrderedType
  - Pair
    
    M
    
    N
  - S
  - UnorderedPair
    
    M
- Predicate
  - Make
    
    Ord
  - OrderedType
  - S
- Range
- Segmenttree
- Store
  - Make
  - S
- Terminal
- Trie
  - Grp
  - Make
    
    Data
  - S
- Unicode
- Unicodetable
- Unionfind
  - Make
    
    M
    
    S
  - MapS
  - PartitionSig
  - SetS
coq-core.config
- Coq_config
coq-core.engine
- EConstr
  - EInstance
  - ESorts
  - Unsafe
  - Vars
- Evar_kinds
- Evarutil
  - VarSet
- Evd
  - Abstraction
  - Filter
  - FutureGoals
  - Identity
  - Metamap
    
    Monad
    
    M
    
    Smart
  - MiniEConstr
    
    EInstance
    
    ESorts
  - Monad
    
    List
  - MonadR
    
    List
  - Store
- Ftactic
  - List
  - Notations
- Logic_monad
  - BackState
  - Logical
    
    List
    
    P
    
    Unsafe
  - NonLogical
    
    List
  - Param
- Namegen
- Nameops
  - Name
  - Subscript
- Proofview
  - Goal
  - Monad
    
    List
  - NonLogical
    
    List
  - Progress
  - Trace
  - Unsafe
  - UnsafeRepr
- Proofview_monad
  - Comb
  - Env
  - Info
  - InfoL
  - Logical
    
    List
    
    Unsafe
  - P
  - Pv
  - Reader
  - Solution
  - State
  - StateStore
  - Status
  - Trace
  - Writer
- Termops
  - Internal
- UState
- UnivGen
- UnivMinim
- UnivNames
- UnivProblem
  - Set
- UnivSubst
coq-core.gramlib
- Gramlib
  - Gramext
  - Grammar
    
    ExtS
    
    Entry
    
    Parsable
    
    Production
    
    Rule
    
    Rules
    
    Symbol
    
    Unsafe
    
    GMake
    
    Entry
    
    L
    
    State
    
    Parsable
    
    Production
    
    Rule
    
    Rules
    
    Symbol
    
    Unsafe
    
    S
    
    Entry
    
    Parsable
    
    Production
    
    Rule
    
    Rules
    
    Symbol
  - Plexing
    
    S
    
    State
coq-core.interp
- Abbreviation
- Constrexpr
- Constrexpr_ops
- Constrextern
- Constrintern
- Decls
- Deprecation
- Dumpglob
- Genintern
  - Store
- Impargs
- Implicit_quantifiers
- Modintern
- Notation
  - NotationMap
    
    Monad
    
    M
    
    Smart
  - SpecificNotationMap
    
    Monad
    
    M
    
    Smart
- Notation_ops
- Notation_term
- NumTok
  - Signed
  - SignedNat
  - Unsigned
  - UnsignedNat
- Reserve
- Smartlocate
- Stdarg
coq-core.kernel
- CClosure
  - RedFlags
- CPrimitives
- Constr
- Context
  - Compacted
    
    Declaration
  - Named
    
    Declaration
  - Rel
    
    Declaration
- Conv_oracle
- Cooking
- Declarations
- Declareops
- Discharge
- Entries
- Environ
  - Globals
  - QConstant
  - QConstruct
  - QGlobRef
  - QInd
  - QMutInd
  - QNameS
  - QProjection
    
    Repr
- Esubst
  - Internal
- Evar
  - Map
    
    Monad
    
    M
    
    Smart
- Float64
- Float64_common
- IndTyping
- Indtypes
- Inductive
- InferCumulativity
- Mod_subst
- Mod_typing
- Modops
- Names
  - Cmap
    
    Monad
    
    M
    
    Smart
  - Cmap_env
    
    Monad
    
    M
    
    Smart
  - Constant
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Constrmap
    
    Monad
    
    M
    
    Smart
  - Constrmap_env
    
    Monad
    
    M
    
    Smart
  - Construct
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Cpred
  - Cset
  - Cset_env
  - DPmap
    
    Monad
    
    M
    
    Smart
  - DirPath
  - EqType
  - GlobRef
    
    CanOrd
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Map_env
    
    Monad
    
    M
    
    Smart
    
    Set
    
    Set_env
    
    SyntacticOrd
    
    UserOrd
  - Id
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Pred
  - Ind
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Indmap
    
    Monad
    
    M
    
    Smart
  - Indmap_env
    
    Monad
    
    M
    
    Smart
  - KNmap
    
    Monad
    
    M
    
    Smart
  - KNpred
  - KNset
  - KerName
  - Label
    
    Map
    
    Monad
    
    M
    
    Smart
  - MBId
  - MBImap
    
    Monad
    
    M
    
    Smart
  - MPmap
    
    Monad
    
    M
    
    Smart
  - Mindmap
    
    Monad
    
    M
    
    Smart
  - Mindmap_env
    
    Monad
    
    M
    
    Set
    
    Smart
  - Mindset
  - ModIdmap
    
    Monad
    
    M
    
    Smart
  - ModPath
  - MutInd
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
  - Name
  - Projection
    
    CanOrd
    
    Repr
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
    
    SyntacticOrd
    
    UserOrd
  - QNameS
    
    CanOrd
    
    SyntacticOrd
    
    UserOrd
- Nativecode
- Nativeconv
- Nativelambda
- Nativelib
- Nativelibrary
- Nativevalues
- Opaqueproof
  - HandleMap
- Parray
- Primred
  - RedNative
    
    E
  - RedNativeEntries
- Reduction
- Relevanceops
- Retroknowledge
- Safe_typing
- Section
- Sorts
- Subtyping
- Term
- Term_typing
- TransparentState
- Type_errors
- Typeops
- UGraph
  - Bound
- Uint63
- Univ
  - AbstractContext
  - Constraints
  - ContextSet
  - Instance
  - Level
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
  - UContext
  - UGlobal
  - Universe
    
    Map
    
    Monad
    
    M
    
    Smart
  - Variance
- Vars
- Vconv
- Vm
- Vmbytecodes
  - Label
- Vmbytegen
- Vmemitcodes
- Vmlambda
- Vmopcodes
- Vmsymtable
- Vmvalues
coq-core.lib
- AcyclicGraph
  - Make
    
    Point
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
  - Point
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
- Aux_file
- CAst
- CDebug
- CErrors
- CProfile
- CWarnings
- Control
- CoqProject_file
- Core_plugins_findlib_compat
- DAst
- Envars
- Feedback
- Flags
- Genarg
  - ArgT
  - GenObj
  - Register
    
    M
- Hook
- LStream
- Loc
- ObjFile
- Pp
- Pp_diff
  - StringDiff
- Rtree
  - Smart
- Spawn
  - Async
    
    ML
  - Control
  - MainLoopModel
  - Sync
- Stateid
- System
- Util
  - Array
    
    Floatarray
    
    Fun1
    
    Smart
    
    Smart
  - Empty
  - List
    
    MonoS
    
    Smart
  - Map
    
    ExtS
    
    Monad
    
    M
    
    Set
    
    Smart
    
    MonadS
    
    OrderedType
  - Set
    
    Hashcons
    
    H
    
    M
    
    HashedType
    
    OrderedType
  - String
    
    List
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Pred
  - Union
coq-core.library
- Coqlib
- Global
- Globnames
  - ExtRefMap
    
    Monad
    
    M
    
    Smart
  - ExtRefOrdered
  - ExtRefSet
- Goptions
  - MakeRefTable
    
    A
    
    Set
  - MakeStringTable
    
    A
  - OptionMap
- Lib
- Libnames
  - Spmap
- Libobject
  - Dyn
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
- Nametab
  - EqualityType
  - GlobDirRef
  - Make
    
    E
    
    U
  - Modules
  - NAMETREE
  - UnivIdMap
    
    Monad
    
    M
    
    Set
    
    Smart
  - UserName
- Summary
  - Dyn
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - Local
coq-core.parsing
- CLexer
  - Error
  - Lexer
    
    State
  - LexerDiff
    
    State
- Extend
- G_constr
- G_prim
- Notation_gram
- Notgram_ops
- Pcoq
  - Constr
  - Entry
  - GramState
  - Lookahead
  - Module
  - Parsable
  - Prim
  - Production
  - Rule
  - Rules
  - Symbol
- Tok
coq-core.plugins.btauto
- Btauto_plugin
  - G_btauto
  - Refl_btauto
    
    Btauto
coq-core.plugins.cc
- Cc_plugin
  - Ccalgo
    
    ATerm
    
    PacMap
    
    PafMap
  - Ccproof
  - Cctac
  - G_congruence
coq-core.plugins.derive
- Derive_plugin
  - Derive
  - G_derive
coq-core.plugins.extraction
- Extraction_plugin
  - Common
  - Extract_env
  - Extraction
  - G_extraction
  - Haskell
  - Json
  - Miniml
  - Mlutil
    
    Mlenv
  - Modutil
  - Ocaml
  - Scheme
  - Table
    
    Refmap'
    
    Refset'
coq-core.plugins.firstorder
- Firstorder_plugin
  - Formula
  - G_ground
  - Ground
  - Instances
  - Rules
  - Sequent
    
    CM
    
    HP
  - Unify
coq-core.plugins.funind
- Funind_plugin
coq-core.plugins.ltac
- Ltac_plugin
  - ComRewrite
  - Coretactics
  - Evar_tactics
  - Extraargs
  - Extratactics
  - G_auto
  - G_class
  - G_eqdecide
  - G_ltac
  - G_obligations
  - G_rewrite
  - G_tactic
  - Internals
  - Leminv
  - Pltac
  - Pptactic
  - Profile_ltac
  - Profile_ltac_tactics
  - Tacarg
  - Taccoerce
    
    Value
  - Tacentries
  - Tacenv
  - Tacexpr
  - Tacintern
  - Tacinterp
    
    TacStore
    
    Value
  - Tacsubst
  - Tactic_debug
  - Tactic_matching
  - Tactic_option
coq-core.plugins.ltac2
- Ltac2_plugin
  - G_ltac2
  - Tac2core
    
    Core
  - Tac2dyn
    
    Arg
    
    ArgMap
    
    M
    
    Param
    
    Val
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - Tac2entries
    
    Pltac
  - Tac2env
  - Tac2expr
  - Tac2extffi
  - Tac2ffi
    
    Valexpr
  - Tac2intern
  - Tac2interp
  - Tac2match
  - Tac2print
  - Tac2qexpr
  - Tac2quote
  - Tac2stdlib
  - Tac2tactics
  - Tac2types
coq-core.plugins.micromega
- Micromega_plugin
  - Certificate
  - Coq_micromega
  - G_micromega
  - Itv
  - Linsolve
  - Micromega
    
    Coq_Pos
    
    N
    
    Pos
    
    Z
  - Mutils
    
    CamlToCoq
    
    Cmp
    
    CoqToCaml
    
    Hash
    
    IMap
    
    ISet
    
    Int
    
    McPrinter
    
    Tag
    
    TagSet
  - NumCompat
    
    Q
    
    Notations
    
    QArith
    
    Notations
    
    Z
    
    Z
    
    ZArith
  - Persistent_cache
    
    PHashtable
  - Polynomial
    
    BoundWithProof
    
    LinPoly
    
    MonT
    
    MonMap
    
    Monomial
    
    Poly
    
    ProofFormat
    
    Env
    
    WithProof
  - Simplex
  - Sos
  - Sos_lib
  - Sos_types
  - Vect
    
    Bound
coq-core.plugins.nsatz
- Nsatz_plugin
  - G_nsatz
  - Ideal
    
    Make
    
    P
    
    Monomial
  - Nsatz
  - Polynom
    
    Coef
    
    Make
    
    C
    
    S
  - Utile
coq-core.plugins.number_string_notation
- Number_string_notation_plugin
coq-core.plugins.ring
- Ring_plugin
  - G_ring
  - Ring
  - Ring_ast
coq-core.plugins.rtauto
- Rtauto_plugin
coq-core.plugins.ssreflect
- Ssreflect_plugin
  - Ssrast
  - Ssrbwd
  - Ssrcommon
    
    MakeState
    
    S
    
    StateType
  - Ssrelim
  - Ssrequality
  - Ssrfwd
  - Ssripats
    
    Internal
  - Ssrparser
  - Ssrprinters
  - Ssrtacticals
  - Ssrvernac
  - Ssrview
    
    AdaptorDb
coq-core.plugins.ssrmatching
- Ssrmatching_plugin
  - G_ssrmatching
  - Ssrmatching
    
    Internal
coq-core.plugins.tauto
- Tauto_plugin
  - Tauto
coq-core.plugins.tutorial.p0
- Tuto0_plugin
  - G_tuto0
  - Tuto0_main
coq-core.plugins.tutorial.p1
- Tuto1_plugin
coq-core.plugins.tutorial.p2
- Tuto2_plugin
coq-core.plugins.tutorial.p3
- Tuto3_plugin
coq-core.plugins.zify
- Zify_plugin
  - G_zify
  - Zify
    
    BinOp
    
    BinOpSpec
    
    BinRel
    
    CstOp
    
    InjTable
    
    PropBinOp
    
    PropUnOp
    
    S
    
    Saturate
    
    UnOp
    
    UnOpSpec
coq-core.pretyping
- Arguments_renaming
- Cases
- Cbv
- Coercion
- Coercionops
- Constr_matching
- Detyping
  - PrintingInductiveMake
    
    Test
- Evarconv
- Evardefine
- Evarsolve
  - AllowedEvars
- Find_subterm
- Geninterp
  - TacStore
  - Val
  - ValTMap
    
    Value
- GlobEnv
- Glob_ops
- Glob_term
- Heads
- Indrec
- Inductiveops
- Keys
- Locus
- Locusops
- Ltac_pretype
- Nativenorm
- Pattern
- Patternops
- Pretype_errors
- Pretyping
- Program
- Reductionops
- Retyping
- Structures
- Tacred
- Typeclasses
- Typeclasses_errors
- Typing
- Unification
- Vnorm
coq-core.printing
- Genprint
- Ppconstr
- Ppextend
- Pputils
- Printer
  - ContextObjectMap
    
    Monad
    
    M
    
    Smart
  - Debug
- Proof_diffs
coq-core.proofs
- Clenv
- Evar_refiner
- Goal
- Goal_select
- Logic
- Miscprint
- Proof
- Proof_bullet
- Refine
- Tacmach
  - Old
- Tactypes
coq-core.stm
- AsyncTaskQueue
  - MakeQueue
    
    T
  - MakeWorker
    
    T
  - Task
- CoqworkmgrApi
- Dag
  - Make
    
    Property
  - S
    
    Property
- Partac
  - TacTask
- ProofBlockDelimiter
- Spawned
- Stm
  - AsyncOpts
  - DynBlockData
    
    Easy
    
    HMap
    
    V1
    
    V2
    
    Map
    
    Value
  - ProofTask
  - QueryTask
- Stmargs
- TQueue
- Vcs
  - Kind
  - Make
    
    Branch
    
    Dag
    
    Property
    
    K
  - S
    
    Branch
    
    Dag
    
    Property
- Vio_checking
- WorkerPool
  - Make
    
    Model
  - PoolModel
coq-core.sysinit
coq-core.tactics
- Abstract
- Auto
- Autorewrite
- Btermdn
  - Make
- Cbn
- Class_tactics
  - Search
- Contradiction
- DeclareScheme
- Dn
  - Make
- Dnet
  - Datatype
  - Make
    
    T
  - S
- Eauto
- Elim
- Elimschemes
- Eqdecide
- Eqschemes
- Equality
- Genredexpr
- Hints
  - FullHint
  - Hint_db
- Hipattern
- Ind_tables
- Inv
- Ppred
- Redexpr
- Redops
- Rewrite
  - Internal
- Tacticals
  - Old
- Tactics
  - New
  - Simple
- Term_dnet
  - IDENT
  - Make
    
    Ident
    
    Opt
  - OPT
  - S
coq-core.top_printers
- Top_printers
coq-core.toplevel
- Ccompile
- Coqc
- Coqcargs
- Coqloop
- Coqrc
- Coqtop
- G_toplevel
  - Toplevel_
- Vernac
  - State
- WorkerLoop
coq-core.vernac
- Assumptions
- Attributes
  - Notations
- Auto_ind_decl
- Canonical
- Classes
  - Internal
- ComArguments
- ComAssumption
- ComCoercion
- ComDefinition
- ComExtraDeps
- ComFixpoint
- ComHints
- ComInductive
  - Internal
  - Mind_decl
- ComPrimitive
- ComProgramFixpoint
- ComSearch
- ComTactic
- DebugHook
  - Action
  - Answer
  - Intf
- Declare
  - CInfo
  - Hook
    
    S
  - Info
  - Internal
    
    Constant
  - OblState
  - Obls
  - Proof
- DeclareInd
  - Internal
- DeclareUctx
- DeclareUniv
- Declaremods
- Egramcoq
- Egramml
- Future
  - UUID
- G_proofs
- G_vernac
- Himsg
- Indschemes
- Library
- Loadpath
- Locality
- Metasyntax
- Mltop
  - PluginSpec
- Opaques
  - Summary
- Ppvernac
- Prettyp
- Printmod
- Proof_using
- Pvernac
  - Unsafe
  - Vernac_
- RecLemmas
- Record
  - Ast
  - Data
  - Internal
  - Record_decl
- RetrieveObl
- Search
- Topfmt
- Vernac_classifier
- Vernacentries
  - Preprocessed_Mind_decl
- Vernacexpr
- Vernacextend
  - InProg
  - InProof
  - OutProg
  - OutProof
- Vernacinterp
- Vernacprop
- Vernacstate
  - Declare
  - LemmaStack
  - Parser
  - Stm
  - System
coq-core.vm
- Coqrun
coqide-server.core
- Document
  - signals
coqide-server.protocol
- Interface
- Richpp
- Serialize
- Xml_lexer
- Xml_parser
- Xml_printer
- Xmlprotocol

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

exception EqNotFound of Names.inductive

exception EqUnknown of string

exception UndefinedCst of string

exception InductiveWithProduct

exception InductiveWithSort

exception ParameterWithoutEquality of Names.GlobRef.t

exception NonSingletonProp of Names.inductive

exception DecidabilityMutualNotSupported

exception NoDecidabilityCoInductive

exception ConstructorWithNonParametricInductiveType of Names.inductive

exception DecidabilityIndicesNotSupported

exception InternalDependencies

val beq_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

Build equivalence between boolean equality and Leibniz equality

val lb_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

val bl_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind

Build decidability of equality

val eq_dec_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind