package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
val is_disjunction : ?strict:bool -> ?onlybinary:bool -> testing_function
val match_with_conjunction : ?strict:bool -> ?onlybinary:bool -> (EConstr.constr * EConstr.constr list) matching_function
val is_conjunction : ?strict:bool -> ?onlybinary:bool -> testing_function
val match_with_record : (EConstr.constr * EConstr.constr list) matching_function
val is_record : testing_function
val match_with_tuple : (EConstr.constr * EConstr.constr list * bool) matching_function
val is_tuple : testing_function
val match_with_empty_type : EConstr.constr matching_function
val is_empty_type : testing_function
val match_with_unit_or_eq_type : EConstr.constr matching_function
val is_unit_or_eq_type : testing_function
val is_unit_type : testing_function
val is_inductive_equality : Names.inductive -> bool
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 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 =
  1. | MonomorphicLeibnizEq of EConstr.constr * EConstr.constr
  2. | PolymorphicLeibnizEq of EConstr.constr * EConstr.constr * EConstr.constr
  3. | HeterogenousEq of EConstr.constr * EConstr.constr * EConstr.constr * EConstr.constr
exception NoEquationFound
val is_matching_sigma : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val is_matching_not : Environ.env -> Evd.evar_map -> EConstr.constr -> bool
val is_matching_imp_False : Environ.env -> Evd.evar_map -> EConstr.constr -> bool