Module Firstorder_plugin.Formula
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
=
|
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 atoms
=
{
positive : EConstr.constr list;
negative : EConstr.constr list;
}
type side
=
|
Hyp
|
Concl
|
Hint
val dummy_id : Names.GlobRef.t
val build_atoms : Environ.env -> Evd.evar_map -> counter -> side -> EConstr.constr -> bool * atoms
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 t
=
{
id : Names.GlobRef.t;
constr : EConstr.constr;
pat : (left_pattern, right_pattern) sum;
atoms : atoms;
}
val build_formula : Environ.env -> Evd.evar_map -> side -> Names.GlobRef.t -> EConstr.types -> counter -> (t, EConstr.types) sum