package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type flags = {
  1. qflag : bool;
  2. reds : RedFlags.reds;
}
val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 'a -> 'a -> 'b -> 'b -> int
val (==?) : ('a -> 'a -> 'b -> 'b -> int) -> ('c -> 'c -> int) -> 'a -> 'a -> 'b -> 'b -> 'c -> 'c -> int
type ('a, 'b) sum =
  1. | Left of 'a
  2. | Right of 'b
type counter = bool -> Constr.metavariable
val construct_nhyps : Environ.env -> Constr.pinductive -> int array
val ind_hyps : Environ.env -> Evd.evar_map -> int -> Constr.pinductive -> EConstr.constr list -> EConstr.rel_context array
module Env : sig ... end
type atom
val hole_atom : atom
val repr_atom : Env.t -> atom -> EConstr.t
val compare_atom : atom -> atom -> int
type atoms = {
  1. positive : atom list;
  2. negative : atom list;
}
type _ side =
  1. | Hyp : bool -> [ `Hyp ] side
  2. | Concl : [ `Goal ] side
type right_pattern =
  1. | Rarrow
  2. | Rand
  3. | Ror
  4. | Rfalse
  5. | Rforall
  6. | Rexists of Constr.metavariable * EConstr.constr * bool
type left_arrow_pattern =
  1. | LLatom
  2. | LLfalse of Constr.pinductive * EConstr.constr list
  3. | LLand of Constr.pinductive * EConstr.constr list
  4. | LLor of Constr.pinductive * EConstr.constr list
  5. | LLforall of EConstr.constr
  6. | LLexists of Constr.pinductive * EConstr.constr list
  7. | LLarrow of EConstr.constr * EConstr.constr * EConstr.constr
type left_pattern =
  1. | Lfalse
  2. | Land of Constr.pinductive
  3. | Lor of Constr.pinductive
  4. | Lforall of Constr.metavariable * EConstr.constr * bool
  5. | Lexists of Constr.pinductive
  6. | LA of atom * left_arrow_pattern
type _ identifier = private
  1. | GoalId : [ `Goal ] identifier
  2. | FormulaId : Names.GlobRef.t -> [ `Hyp ] identifier
val goal_id : [ `Goal ] identifier
val formula_id : Environ.env -> Names.GlobRef.t -> [ `Hyp ] identifier
type _ pattern =
  1. | LeftPattern : left_pattern -> [ `Hyp ] pattern
  2. | RightPattern : right_pattern -> [ `Goal ] pattern
type 'a t = private {
  1. id : 'a identifier;
  2. constr : atom;
  3. pat : 'a pattern;
  4. atoms : atoms;
}
type any_formula =
  1. | AnyFormula : 'a t -> any_formula
val build_formula : flags:flags -> Env.t -> Environ.env -> Evd.evar_map -> 'a side -> 'a identifier -> EConstr.types -> counter -> Env.t * ('a t, atom) sum
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