package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val qflag : bool Stdlib.ref
val red_flags : CClosure.RedFlags.reds Stdlib.ref
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
type atoms = {
  1. positive : EConstr.constr list;
  2. negative : EConstr.constr list;
}
type side =
  1. | Hyp
  2. | Concl
  3. | Hint
val dummy_id : Names.GlobRef.t
val build_atoms : Environ.env -> Evd.evar_map -> counter -> side -> EConstr.constr -> bool * atoms
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 EConstr.constr * left_arrow_pattern
type t = {
  1. id : Names.GlobRef.t;
  2. constr : EConstr.constr;
  3. pat : (left_pattern, right_pattern) sum;
  4. atoms : atoms;
}
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