Module Firstorder_core_plugin.Formula

type flags = {
  1. 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 repr_atom : Env.t -> atom -> EConstr.t
val compare_atom : atom -> atom -> int
val meta_in_atom : Constr.metavariable -> atom -> bool
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 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 uid
val eq_uid : uid -> uid -> bool
type _ pattern =
  1. | LeftPattern : left_pattern -> [ `Hyp ] pattern
  2. | RightPattern : right_pattern -> [ `Goal ] pattern
type 'a t = private {
  1. id : 'a identifier;
  2. uid : uid;
  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