package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module DeclsSource

Sourcetype theorem_kind =
  1. | Theorem
  2. | Lemma
  3. | Fact
  4. | Remark
  5. | Property
  6. | Proposition
  7. | Corollary
Sourcetype 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
Sourcetype assumption_object_kind =
  1. | Definitional
  2. | Logical
  3. | Conjectural
  4. | Context

Kinds used in library

Sourcetype 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

Sourcetype variable_data = {
  1. opaque : bool;
  2. kind : logical_kind;
}
Sourceval add_variable_data : Names.variable -> variable_data -> unit
Sourceval variable_secpath : Names.variable -> Libnames.qualid
Sourceval variable_kind : Names.variable -> logical_kind
Sourceval variable_opacity : Names.variable -> bool
Sourceval 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