package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type theorem_kind =
  1. | Theorem
  2. | Lemma
  3. | Fact
  4. | Remark
  5. | Property
  6. | Proposition
  7. | Corollary
type definition_object_kind =
  1. | Definition
  2. | Coercion
  3. | SubClass
  4. | CanonicalStructure
  5. | Example
  6. | Fixpoint
  7. | CoFixpoint
  8. | Scheme
  9. | StructureComponent
  10. | IdentityCoercion
  11. | Instance
  12. | Method
  13. | Let
type assumption_object_kind =
  1. | Definitional
  2. | Logical
  3. | Conjectural
  4. | Context

Kinds used in library

type logical_kind =
  1. | IsPrimitive
  2. | IsAssumption of assumption_object_kind
  3. | IsDefinition of definition_object_kind
  4. | IsProof of theorem_kind

This module manages non-kernel informations about declarations. It is either non-logical informations or logical informations that have no place to be (yet) in the kernel

Registration and access to the table of variable

type variable_data = {
  1. opaque : bool;
  2. kind : logical_kind;
}
val add_variable_data : Names.variable -> variable_data -> unit
val variable_secpath : Names.variable -> Libnames.qualid
val variable_kind : Names.variable -> logical_kind
val variable_opacity : Names.variable -> bool
val variable_exists : Names.variable -> bool
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct