Module Firstorder_plugin.Formula

type flags = {
qflag : bool;
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 =
| Left of 'a
| 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 atom
val repr_atom : atom -> EConstr.t
type atoms = {
positive : atom list;
negative : atom list;
}
type _ side =
| Hyp : bool -> [ `Hyp ] side
| Concl : [ `Goal ] side
type right_pattern =
| Rarrow
| Rand
| Ror
| Rfalse
| Rforall
| Rexists of Constr.metavariable * EConstr.constr * bool
type left_arrow_pattern =
| LLatom
| LLfalse of Constr.pinductive * EConstr.constr list
| LLand of Constr.pinductive * EConstr.constr list
| LLor of Constr.pinductive * EConstr.constr list
| LLforall of EConstr.constr
| LLexists of Constr.pinductive * EConstr.constr list
| LLarrow of EConstr.constr * EConstr.constr * EConstr.constr
type left_pattern =
| Lfalse
| Land of Constr.pinductive
| Lor of Constr.pinductive
| Lforall of Constr.metavariable * EConstr.constr * bool
| Lexists of Constr.pinductive
| LA of EConstr.constr * left_arrow_pattern
type _ identifier = private
| GoalId : [ `Goal ] identifier
| FormulaId : Names.GlobRef.t -> [ `Hyp ] identifier
val goal_id : [ `Goal ] identifier
val formula_id : Environ.env -> Names.GlobRef.t -> [ `Hyp ] identifier
type _ pattern =
| LeftPattern : left_pattern -> [ `Hyp ] pattern
| RightPattern : right_pattern -> [ `Goal ] pattern
type 'a t = private {
id : 'a identifier;
constr : EConstr.constr;
pat : 'a pattern;
atoms : atoms;
}
type any_formula =
| AnyFormula : 'a t -> any_formula
val build_formula : flags:flags -> Environ.env -> Evd.evar_map -> 'a side -> 'a identifier -> EConstr.types -> counter -> ('a t, atom) sum