(* -------------------------------------------------------------------- *)
open EcSymbols
open EcPath
(* -------------------------------------------------------------------- *)
(* Symbols with dedicated parsing rules *)
val s_get : symbol
val s_set : symbol
val s_nil : symbol
val s_cons : symbol
val s_abs : symbol
val is_mixfix_op : symbol -> bool
val s_dbool : qsymbol
val s_dbitstring : qsymbol
val s_dinter : qsymbol
val s_real_of_int : qsymbol
(* -------------------------------------------------------------------- *)
val i_top : symbol
val i_self : symbol
val p_top : path
(* -------------------------------------------------------------------- *)
val i_Pervasive : symbol
val p_Pervasive : path
(* -------------------------------------------------------------------- *)
val base_rnd : string
val base_ll : string
(* -------------------------------------------------------------------- *)
module CI_Unit : sig
val p_unit : path
val p_tt : path
end
(*-------------------------------------------------------------------- *)
module CI_Witness : sig
val p_witness : path
end
(* -------------------------------------------------------------------- *)
module CI_Option : sig
val p_option : path
val p_none : path
val p_some : path
val p_oget : path
end
(*-------------------------------------------------------------------- *)
module CI_Bool : sig
val i_Bool : symbol
val p_Bool : path
val p_bool : path
val p_true : path
val p_false : path
val p_not : path
val p_anda : path
val p_and : path
val p_ora : path
val p_or : path
val p_imp : path
val p_iff : path
val p_eq : path
end
(* -------------------------------------------------------------------- *)
module CI_Int : sig
val i_Int : symbol
val p_Int : path
val p_int : path
val p_int_elim : path
val p_int_opp : path
val p_int_add : path
val p_int_mul : path
val p_int_le : path
val p_int_lt : path
val p_int_pow : path
val p_int_edivz : path
val p_int_max : path
val p_iteri : path
end
(* -------------------------------------------------------------------- *)
module CI_Cost : sig
val i_Cost : string
val p_Cost : path
val p_cost : path
val p_cost_inf : path
val p_cost_opp : path
val p_cost_add : path
val p_cost_scale : path
val p_cost_xscale : path
val p_cost_le : path
val p_cost_lt : path
val p_cost_subcond : path
val p_cost_is_int : path
end
(* -------------------------------------------------------------------- *)
module CI_Xint : sig
val p_Xint : path
val p_xint : path
val p_N : path
val p_inf : path
val p_xopp : path
val p_xadd : path
val p_xmul : path
val p_xmuli : path
val p_xle : path
val p_xlt : path
val p_xmax : path
val p_is_int : path
val p_is_inf : path
val p_xoget : path
val p_choaretac : path
val p_Bigxint : path
val p_Bigcost : path
val p_bigx : path
val p_bigcost : path
end
(* -------------------------------------------------------------------- *)
module CI_Real : sig
val i_Real : symbol
val p_Real : path
val p_real : path
val p_RealExtra : path
val p_RealOrder : path
val p_real0 : path
val p_real1 : path
val p_real_opp : path
val p_real_add : path
val p_real_mul : path
val p_real_inv : path
val p_real_pow : path
val p_real_le : path
val p_real_lt : path
val p_real_of_int : path
val p_real_abs : path
val real_lemma : string -> path
val real_order_lemma : string -> path
end
(* -------------------------------------------------------------------- *)
module CI_Pred : sig
val i_Pred : symbol
val p_Pred : path
val p_predT : path
val p_pred1 : path
end
(* -------------------------------------------------------------------- *)
module CI_Distr : sig
val i_Distr : symbol
val p_Distr : path
val p_distr : path
val p_dbool : path
val p_dbitstring : path
val p_dinter : path
val p_dunit : path
val p_dlet : path
val p_dmap : path
val p_support : path
val p_mu : path
val p_lossless: path
val p_uniform : path
val p_full : path
val p_dfold : path
end
(* -------------------------------------------------------------------- *)
module CI_Sum : sig
val i_Sum : symbol
val p_Sum : path
val p_sum : path
end
(* -------------------------------------------------------------------- *)
module CI_Map : sig
val i_Map : symbol
val p_Map : path
val p_map : path
val p_get : path
val p_set : path
val p_cst : path
end
(* -------------------------------------------------------------------- *)
module CI_Logic : sig
val i_Logic : symbol
val p_Logic : path
val mk_logic : symbol -> path
val p_unit_elim : path
val p_false_elim : path
val p_bool_elim : path
val p_and_elim : path
val p_anda_elim : path
val p_and_proj_l : path
val p_and_proj_r : path
val p_anda_proj_l : path
val p_anda_proj_r : path
val p_or_elim : path
val p_ora_elim : path
val p_iff_elim : path
val p_if_elim : path
val p_true_intro : path
val p_and_intro : path
val p_anda_intro : path
val p_or_intro_l : path
val p_ora_intro_l : path
val p_or_intro_r : path
val p_ora_intro_r : path
val p_iff_intro : path
val p_if_intro : path
val p_if_congr : path
val p_eq_refl : path
val p_eq_iff : path
val p_eq_trans : path
val p_eq_ind : path
val p_fcongr : path
val p_eq_sym : path
val p_eq_sym_imp : path
val p_eq_iff_imp : path
val p_negeqF : path
val p_iff_lr : path
val p_iff_rl : path
val p_cut_lemma : path
val p_case_eq_bool : path
val p_ip_dup : path
val p_negbTE : path
end