Module `Hipattern`

type 'a matching_function = Environ.env -> Evd.evar_map -> EConstr.constr -> 'a option
type testing_function = Environ.env -> Evd.evar_map -> EConstr.constr -> bool

val match_with_non_recursive_type : (EConstr.constr * EConstr.constr list) matching_function
val is_non_recursive_type : testing_function
val match_with_disjunction : ?⁠strict:bool -> ?⁠onlybinary:bool -> (EConstr.constr * EConstr.constr list) matching_function: Non recursive type with no indices and exactly one argument for each constructor; canonical definition of n-ary disjunction if strict

val is_disjunction : ?⁠strict:bool -> ?⁠onlybinary:bool -> testing_function
val match_with_conjunction : ?⁠strict:bool -> ?⁠onlybinary:bool -> (EConstr.constr * EConstr.constr list) matching_function: Non recursive tuple (one constructor and no indices) with no inner dependencies; canonical definition of n-ary conjunction if strict

val is_conjunction : ?⁠strict:bool -> ?⁠onlybinary:bool -> testing_function
val match_with_record : (EConstr.constr * EConstr.constr list) matching_function: Non recursive tuple, possibly with inner dependencies

val is_record : testing_function
val match_with_tuple : (EConstr.constr * EConstr.constr list * bool) matching_function: Like record but supports and tells if recursive (e.g. Acc)

val is_tuple : testing_function
val match_with_empty_type : EConstr.constr matching_function: No constructor, possibly with indices

val is_empty_type : testing_function
val match_with_unit_or_eq_type : EConstr.constr matching_function: type with only one constructor and no arguments, possibly with indices

val is_unit_or_eq_type : testing_function
val is_unit_type : testing_function: type with only one constructor and no arguments, no indices

val is_inductive_equality : Names.inductive -> bool: type with only one constructor, no arguments and at least one dependency

val match_with_equality_type : (EConstr.constr * EConstr.constr list) matching_function
val is_equality_type : testing_function
val match_with_nottype : (EConstr.constr * EConstr.constr) matching_function
val is_nottype : testing_function
val match_with_forall_term : (Names.Name.t Context.binder_annot * EConstr.constr * EConstr.constr) matching_function
val is_forall_term : testing_function
val match_with_imp_term : (EConstr.constr * EConstr.constr) matching_function
val is_imp_term : testing_function

val has_nodep_prod_after : int -> testing_function
val has_nodep_prod : testing_function
val match_with_nodep_ind : (EConstr.constr * EConstr.constr list * int) matching_function
val is_nodep_ind : testing_function
val match_with_sigma_type : (EConstr.constr * EConstr.constr list) matching_function
val is_sigma_type : testing_function

type equation_kind = | MonomorphicLeibnizEq of EConstr.constr * EConstr.constr | PolymorphicLeibnizEq of EConstr.constr * EConstr.constr * EConstr.constr | HeterogenousEq of EConstr.constr * EConstr.constr * EConstr.constr * EConstr.constr

val match_with_equation : Environ.env -> Evd.evar_map -> EConstr.constr -> Coqlib.coq_eq_data option * EConstr.constr * equation_kind
val find_eq_data_decompose : Environ.env -> Evd.evar_map -> EConstr.constr -> Coqlib.coq_eq_data * EConstr.EInstance.t * (EConstr.types * EConstr.constr * EConstr.constr): Match terms eq A t u, identity A t u or JMeq A t A u Returns associated lemmas and A,t,u or fails PatternMatchingFailure

val find_this_eq_data_decompose : Environ.env -> Evd.evar_map -> EConstr.constr -> Coqlib.coq_eq_data * EConstr.EInstance.t * (EConstr.types * EConstr.constr * EConstr.constr): Idem but fails with an error message instead of PatternMatchingFailure

val find_eq_data : Evd.evar_map -> EConstr.constr -> Coqlib.coq_eq_data * EConstr.EInstance.t * equation_kind: A variant that returns more informative structure on the equality found

val find_sigma_data_decompose : Environ.env -> Evd.evar_map -> EConstr.constr -> Coqlib.coq_sigma_data * (EConstr.EInstance.t * EConstr.constr * EConstr.constr * EConstr.constr * EConstr.constr): Match a term of the form (existT A P t p) Returns associated lemmas and A,P,t,p

val match_sigma : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr * EConstr.constr: Match a term of the form {x:A|P}, returns A and P

val is_matching_sigma : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val match_eqdec : Environ.env -> Evd.evar_map -> EConstr.constr -> bool * Names.GlobRef.t * EConstr.constr * EConstr.constr * EConstr.constr: Match a decidable equality judgement (e.g {t=u:>T}+{~t=u}), returns t,u,T and a boolean telling if equality is on the left side

val is_matching_not : Environ.env -> Evd.evar_map -> EConstr.constr -> bool: Match a negation

val is_matching_imp_False : Environ.env -> Evd.evar_map -> EConstr.constr -> bool