package coq

  1. Overview
  2. Docs
Package contains no libraries
type locality =
  1. | Discharge
  2. | Local
  3. | Global
type binding_kind =
  1. | Explicit
  2. | Implicit
type polymorphic = bool
type private_flag = bool
type cumulative_inductive_flag = bool
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
type assumption_object_kind =
  1. | Definitional
  2. | Logical
  3. | Conjectural
type assumption_kind = locality * polymorphic * assumption_object_kind
type definition_kind = locality * polymorphic * definition_object_kind
type goal_object_kind =
  1. | DefinitionBody of definition_object_kind
  2. | Proof of theorem_kind
type logical_kind =
  1. | IsAssumption of assumption_object_kind
  2. | IsDefinition of definition_object_kind
  3. | IsProof of theorem_kind
type recursivity_kind =
  1. | Finite
  2. | CoFinite
  3. | BiFinite
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