CoqApprox libraries


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1154 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (8 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (451 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (44 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (25 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (8 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (5 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (33 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (272 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (77 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (95 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (105 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (16 entries)

Global Index

B

BaseOps [module, in CoqApprox.poly_datatypes]
BaseOps.T [axiom, in CoqApprox.poly_datatypes]
BaseOps.tadd [axiom, in CoqApprox.poly_datatypes]
BaseOps.tmul [axiom, in CoqApprox.poly_datatypes]
BaseOps.tone [axiom, in CoqApprox.poly_datatypes]
BaseOps.topp [axiom, in CoqApprox.poly_datatypes]
BaseOps.tsub [axiom, in CoqApprox.poly_datatypes]
BaseOps.tzero [axiom, in CoqApprox.poly_datatypes]
BaseOps.U [axiom, in CoqApprox.poly_datatypes]
BaseOps0 [module, in CoqApprox.poly_datatypes]
BaseZ [module, in CoqApprox.coeff_inst]
BaseZ.T [definition, in CoqApprox.coeff_inst]
BaseZ.tadd [definition, in CoqApprox.coeff_inst]
BaseZ.tmul [definition, in CoqApprox.coeff_inst]
BaseZ.tone [definition, in CoqApprox.coeff_inst]
BaseZ.topp [definition, in CoqApprox.coeff_inst]
BaseZ.tsub [definition, in CoqApprox.coeff_inst]
BaseZ.tzero [definition, in CoqApprox.coeff_inst]
BaseZ.U [definition, in CoqApprox.coeff_inst]
--> _ [notation, in CoqApprox.coeff_inst]
basic_rec [library]
behead_recNdown [lemma, in CoqApprox.basic_rec]
behead_rev_take [lemma, in CoqApprox.basic_rec]
behead_rcons [lemma, in CoqApprox.basic_rec]
behead_rec2down_again [lemma, in CoqApprox.basic_rec]
behead_rec2down [lemma, in CoqApprox.basic_rec]
behead_loop2 [lemma, in CoqApprox.basic_rec]
behead_rec1down [lemma, in CoqApprox.basic_rec]
bigXadd_bigRplus [lemma, in CoqApprox.xreal_ssr_compat]
bigXadd_Xreal_i [lemma, in CoqApprox.xreal_ssr_compat]
bigXadd_Xreal1 [lemma, in CoqApprox.xreal_ssr_compat]
bigXadd_Xreal [lemma, in CoqApprox.xreal_ssr_compat]
bigXadd_Xnan_i [lemma, in CoqApprox.xreal_ssr_compat]
bigXadd_Xnan [lemma, in CoqApprox.xreal_ssr_compat]
big_Xmul_Xadd_distr [lemma, in CoqApprox.xreal_ssr_compat]


C

C [module, in CoqApprox.test_exp_sin]
Cab [abbreviation, in CoqApprox.taylor_thm]
catrev' [definition, in CoqApprox.basic_rec]
coeff_inst [library]
cons_Tuple [definition, in CoqApprox.nary_tuple]
contains_Xnan [lemma, in CoqApprox.xreal_ssr_compat]
contains_subset [lemma, in CoqApprox.interval_compl]
contains_trans [lemma, in CoqApprox.interval_compl]
continuity_pt_sum [lemma, in CoqApprox.taylor_thm]
continuity_pt_eq [lemma, in CoqApprox.taylor_thm]
Cor_Taylor_Lagrange [lemma, in CoqApprox.taylor_thm]
cst_var [section, in CoqApprox.derive_compl]


D

DefixN [section, in CoqApprox.basic_rec]
DefixN.F [variable, in CoqApprox.basic_rec]
DefixN.F1 [variable, in CoqApprox.basic_rec]
DefixN.init [variable, in CoqApprox.basic_rec]
DefixN.N [variable, in CoqApprox.basic_rec]
DefixN.T [variable, in CoqApprox.basic_rec]
Defix1 [section, in CoqApprox.basic_rec]
Defix1.a0 [variable, in CoqApprox.basic_rec]
Defix1.d [variable, in CoqApprox.basic_rec]
Defix1.F [variable, in CoqApprox.basic_rec]
Defix1.T [variable, in CoqApprox.basic_rec]
Defix2 [section, in CoqApprox.basic_rec]
Defix2.a0 [variable, in CoqApprox.basic_rec]
Defix2.a1 [variable, in CoqApprox.basic_rec]
Defix2.d [variable, in CoqApprox.basic_rec]
Defix2.F [variable, in CoqApprox.basic_rec]
Defix2.T [variable, in CoqApprox.basic_rec]
derivable_pt_lim_aux [lemma, in CoqApprox.taylor_thm]
derivable_pt_lim_sum [lemma, in CoqApprox.taylor_thm]
derive_compl [library]


E

eqr [definition, in CoqApprox.Rstruct]
eqrP [lemma, in CoqApprox.Rstruct]
eqX [definition, in CoqApprox.xreal_ssr_compat]
eqXP [lemma, in CoqApprox.xreal_ssr_compat]
eq_foldr [lemma, in CoqApprox.poly_inst_seq]
eq_from_Tnth [lemma, in CoqApprox.nary_tuple]
ExactFullOps [module, in CoqApprox.poly_datatypes]
ExactMonomPolyOps [module, in CoqApprox.poly_datatypes]
ExactSeqPolyMonomUp [module, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.Cadd_addlaw [definition, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.Cadd_comm [definition, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.Cadd_monoid [definition, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.Cmul_comm [definition, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.Cmul_monoid [definition, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.Ctpow [abbreviation, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.is_horner [lemma, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.M [module, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.mask_big_helper [lemma, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.mul_coeffE [lemma, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.tmul_tail_nth [lemma, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.tmul_trunc_nth [lemma, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.trunc_leq [lemma, in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.trunc_inc [lemma, in CoqApprox.poly_inst_seq]


F

F [module, in CoqApprox.test_exp_sin]
factz [definition, in CoqApprox.basic_rec]
fact_zeroF [lemma, in CoqApprox.xreal_ssr_compat]
fibz [definition, in CoqApprox.basic_rec]
FloatIntervalOps [module, in CoqApprox.taylor_model_float_sharp]
FloatMonomPolyOps [module, in CoqApprox.rpa_inst]
FloatMonomPolyOps.Fl [module, in CoqApprox.rpa_inst]
FloatPolyOps [module, in CoqApprox.rpa_inst]
FloatPolyOps.Fl [module, in CoqApprox.rpa_inst]
Fold [section, in CoqApprox.seq_compl]
foldl_cons0 [lemma, in CoqApprox.seq_compl]
foldl_cons [lemma, in CoqApprox.seq_compl]
foldr_cons0 [lemma, in CoqApprox.seq_compl]
foldr_cons [lemma, in CoqApprox.seq_compl]
Fold.A [variable, in CoqApprox.seq_compl]
Fold.B [variable, in CoqApprox.seq_compl]
Fold.f [variable, in CoqApprox.seq_compl]
FullInt [module, in CoqApprox.coeff_inst]
FullInt.T [definition, in CoqApprox.coeff_inst]
FullInt.tadd [definition, in CoqApprox.coeff_inst]
FullInt.tcos [definition, in CoqApprox.coeff_inst]
FullInt.tcst [definition, in CoqApprox.coeff_inst]
FullInt.tdiv [definition, in CoqApprox.coeff_inst]
FullInt.texp [definition, in CoqApprox.coeff_inst]
FullInt.tinv [definition, in CoqApprox.coeff_inst]
FullInt.tinvsqrt [definition, in CoqApprox.coeff_inst]
FullInt.tmul [definition, in CoqApprox.coeff_inst]
FullInt.tnat [definition, in CoqApprox.coeff_inst]
FullInt.tone [definition, in CoqApprox.coeff_inst]
FullInt.topp [definition, in CoqApprox.coeff_inst]
FullInt.tpower_int [definition, in CoqApprox.coeff_inst]
FullInt.tsin [definition, in CoqApprox.coeff_inst]
FullInt.tsqr [definition, in CoqApprox.coeff_inst]
FullInt.tsqrt [definition, in CoqApprox.coeff_inst]
FullInt.tsub [definition, in CoqApprox.coeff_inst]
FullInt.tzero [definition, in CoqApprox.coeff_inst]
FullInt.U [definition, in CoqApprox.coeff_inst]
FullInt.zero_correct [lemma, in CoqApprox.coeff_inst]
FullOps [module, in CoqApprox.poly_datatypes]
FullOps0 [module, in CoqApprox.poly_datatypes]
FullReal [module, in CoqApprox.coeff_inst]
FullReal.T [definition, in CoqApprox.coeff_inst]
FullReal.tadd [definition, in CoqApprox.coeff_inst]
FullReal.tcos [definition, in CoqApprox.coeff_inst]
FullReal.tcst [definition, in CoqApprox.coeff_inst]
FullReal.tdiv [definition, in CoqApprox.coeff_inst]
FullReal.texp [definition, in CoqApprox.coeff_inst]
FullReal.tinv [definition, in CoqApprox.coeff_inst]
FullReal.tinvsqrt [definition, in CoqApprox.coeff_inst]
FullReal.tmul [definition, in CoqApprox.coeff_inst]
FullReal.tnat [definition, in CoqApprox.coeff_inst]
FullReal.tone [definition, in CoqApprox.coeff_inst]
FullReal.topp [definition, in CoqApprox.coeff_inst]
FullReal.tpower_int [definition, in CoqApprox.coeff_inst]
FullReal.tsin [definition, in CoqApprox.coeff_inst]
FullReal.tsqr [definition, in CoqApprox.coeff_inst]
FullReal.tsqrt [definition, in CoqApprox.coeff_inst]
FullReal.tsub [definition, in CoqApprox.coeff_inst]
FullReal.tzero [definition, in CoqApprox.coeff_inst]
FullReal.U [definition, in CoqApprox.coeff_inst]
--> _ [notation, in CoqApprox.coeff_inst]
FullXR [module, in CoqApprox.coeff_inst]
FullXR.big_distrr_spec [lemma, in CoqApprox.coeff_inst]
FullXR.mask_comm [lemma, in CoqApprox.coeff_inst]
FullXR.mask_idemp [lemma, in CoqApprox.coeff_inst]
FullXR.mask_mul_r [lemma, in CoqApprox.coeff_inst]
FullXR.mask_mul_l [lemma, in CoqApprox.coeff_inst]
FullXR.mask_add_r [lemma, in CoqApprox.coeff_inst]
FullXR.mask_add_l [lemma, in CoqApprox.coeff_inst]
FullXR.mask0mul_r [lemma, in CoqApprox.coeff_inst]
FullXR.mask0mul_l [lemma, in CoqApprox.coeff_inst]
FullXR.T [definition, in CoqApprox.coeff_inst]
FullXR.tadd [definition, in CoqApprox.coeff_inst]
FullXR.tadd_assoc [lemma, in CoqApprox.coeff_inst]
FullXR.tadd_comm [lemma, in CoqApprox.coeff_inst]
FullXR.tadd_zeror [lemma, in CoqApprox.coeff_inst]
FullXR.tadd_zerol [lemma, in CoqApprox.coeff_inst]
FullXR.tcos [definition, in CoqApprox.coeff_inst]
FullXR.tcst [definition, in CoqApprox.coeff_inst]
FullXR.tdiv [definition, in CoqApprox.coeff_inst]
FullXR.texp [definition, in CoqApprox.coeff_inst]
FullXR.tinv [definition, in CoqApprox.coeff_inst]
FullXR.tinvsqrt [definition, in CoqApprox.coeff_inst]
FullXR.tmul [definition, in CoqApprox.coeff_inst]
FullXR.tmul_distrr [lemma, in CoqApprox.coeff_inst]
FullXR.tmul_distrl [lemma, in CoqApprox.coeff_inst]
FullXR.tmul_assoc [lemma, in CoqApprox.coeff_inst]
FullXR.tmul_comm [lemma, in CoqApprox.coeff_inst]
FullXR.tmul_oner [lemma, in CoqApprox.coeff_inst]
FullXR.tmul_onel [lemma, in CoqApprox.coeff_inst]
FullXR.tnat [definition, in CoqApprox.coeff_inst]
FullXR.tone [definition, in CoqApprox.coeff_inst]
FullXR.topp [definition, in CoqApprox.coeff_inst]
FullXR.tpow [definition, in CoqApprox.coeff_inst]
FullXR.tpower_int [definition, in CoqApprox.coeff_inst]
FullXR.tpow_opp [lemma, in CoqApprox.coeff_inst]
FullXR.tpow_S [lemma, in CoqApprox.coeff_inst]
FullXR.tpow_0 [lemma, in CoqApprox.coeff_inst]
FullXR.tsin [definition, in CoqApprox.coeff_inst]
FullXR.tsqr [definition, in CoqApprox.coeff_inst]
FullXR.tsqrt [definition, in CoqApprox.coeff_inst]
FullXR.tsub [definition, in CoqApprox.coeff_inst]
FullXR.tzero [definition, in CoqApprox.coeff_inst]
FullXR.U [definition, in CoqApprox.coeff_inst]
--> _ [notation, in CoqApprox.coeff_inst]


G

generic [section, in CoqApprox.derive_compl]


H

hb [definition, in CoqApprox.seq_compl]
head_loopN [lemma, in CoqApprox.basic_rec]
head_rec2down [lemma, in CoqApprox.basic_rec]
head_loop2 [lemma, in CoqApprox.basic_rec]
head_rec1down [lemma, in CoqApprox.basic_rec]
head_loop1 [lemma, in CoqApprox.basic_rec]
head_cons [lemma, in CoqApprox.seq_compl]
Head_Last.d [variable, in CoqApprox.seq_compl]
Head_Last.T [variable, in CoqApprox.seq_compl]
Head_Last [section, in CoqApprox.seq_compl]
hide_let [definition, in CoqApprox.basic_rec]


I

I [module, in CoqApprox.test_exp_sin]
IIbnd [abbreviation, in CoqApprox.interval_compl]
IInan [abbreviation, in CoqApprox.interval_compl]
inhR [lemma, in CoqApprox.Rstruct]
interval_compl [library]
IntMonomPolyOps [module, in CoqApprox.rpa_inst]
IntMonomPolyOps.Int [module, in CoqApprox.rpa_inst]
IntPolyOps [module, in CoqApprox.rpa_inst]
IntPolyOps.Int [module, in CoqApprox.rpa_inst]
intro_unit_R [lemma, in CoqApprox.Rstruct]
inverse [section, in CoqApprox.derive_compl]
iota_Tuple [definition, in CoqApprox.nary_tuple]
Irnd [definition, in CoqApprox.test_exp_sin]


L

lastN [definition, in CoqApprox.nary_tuple]
lastN_Ttoseq [lemma, in CoqApprox.nary_tuple]
last_rev [lemma, in CoqApprox.seq_compl]
left_distr_Xmul_Xadd [lemma, in CoqApprox.xreal_ssr_compat]
Link [module, in CoqApprox.test_exp_sin]
LinkIntX [module, in CoqApprox.rpa_inst]
LinkIntXPr [module, in CoqApprox.poly_inst_seq]
LinkIntXPr.Pol [module, in CoqApprox.poly_inst_seq]
LinkIntXPr.PolX [module, in CoqApprox.poly_inst_seq]
LinkIntX.contains_pointwise [definition, in CoqApprox.rpa_inst]
LinkIntX.contains_pointwise_until [definition, in CoqApprox.rpa_inst]
LinkIntX.link_tmul_tail [axiom, in CoqApprox.rpa_inst]
LinkIntX.link_tmul_trunc [axiom, in CoqApprox.rpa_inst]
LinkSeqPolyMonomUp [module, in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.contains_pointwise [definition, in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.contains_pointwise_until [definition, in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.link_tnth_set_nth_nil [lemma, in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.link_tsize_set_nth_nil [lemma, in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.link_tmul_tail [lemma, in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.link_tmul_trunc [lemma, in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.Pol [module, in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.PolX [module, in CoqApprox.poly_inst_seq]
loopN [definition, in CoqApprox.basic_rec]
loopNE [lemma, in CoqApprox.basic_rec]
loopNS_ex [lemma, in CoqApprox.basic_rec]
loop1 [definition, in CoqApprox.basic_rec]
loop1E [lemma, in CoqApprox.basic_rec]
loop1SE [lemma, in CoqApprox.basic_rec]
loop1S_ex [lemma, in CoqApprox.basic_rec]
loop2 [definition, in CoqApprox.basic_rec]
loop2E [lemma, in CoqApprox.basic_rec]
loop2S_ex [lemma, in CoqApprox.basic_rec]
ltn_subr [lemma, in CoqApprox.seq_compl]


M

map_Tuple [definition, in CoqApprox.nary_tuple]
map_Tnth_enum [lemma, in CoqApprox.nary_tuple]
map2 [definition, in CoqApprox.seq_compl]
Map2 [section, in CoqApprox.seq_compl]
Map2.A [variable, in CoqApprox.seq_compl]
Map2.B [variable, in CoqApprox.seq_compl]
Map2.C [variable, in CoqApprox.seq_compl]
Map2.f [variable, in CoqApprox.seq_compl]
MaskBaseF [module, in CoqApprox.coeff_inst]
MaskBaseF_NE.tcst [definition, in CoqApprox.coeff_inst]
MaskBaseF_NE.tsub [definition, in CoqApprox.coeff_inst]
MaskBaseF_NE.topp [definition, in CoqApprox.coeff_inst]
MaskBaseF_NE.tmul [definition, in CoqApprox.coeff_inst]
MaskBaseF_NE.tadd [definition, in CoqApprox.coeff_inst]
MaskBaseF_NE.tone [definition, in CoqApprox.coeff_inst]
MaskBaseF_NE.tzero [definition, in CoqApprox.coeff_inst]
MaskBaseF_NE.T [definition, in CoqApprox.coeff_inst]
MaskBaseF_NE.U [definition, in CoqApprox.coeff_inst]
MaskBaseF_NE [module, in CoqApprox.coeff_inst]
MaskBaseF.T [definition, in CoqApprox.coeff_inst]
MaskBaseF.tadd [definition, in CoqApprox.coeff_inst]
MaskBaseF.tcst [definition, in CoqApprox.coeff_inst]
MaskBaseF.tmul [definition, in CoqApprox.coeff_inst]
MaskBaseF.tone [definition, in CoqApprox.coeff_inst]
MaskBaseF.topp [definition, in CoqApprox.coeff_inst]
MaskBaseF.tsub [definition, in CoqApprox.coeff_inst]
MaskBaseF.tzero [definition, in CoqApprox.coeff_inst]
MaskBaseF.U [definition, in CoqApprox.coeff_inst]
MaskBaseOps [module, in CoqApprox.poly_datatypes]
MaskBaseOps0 [module, in CoqApprox.poly_datatypes]
minnl [lemma, in CoqApprox.seq_compl]
minnr [lemma, in CoqApprox.seq_compl]
mkTuple [definition, in CoqApprox.nary_tuple]
mkTupleO [definition, in CoqApprox.nary_tuple]
MonomPolyOps [module, in CoqApprox.poly_datatypes]


N

NaryTuple [section, in CoqApprox.nary_tuple]
NaryTupleCast [section, in CoqApprox.nary_tuple]
NaryTupleCast.T [variable, in CoqApprox.nary_tuple]
NaryTupleMap [section, in CoqApprox.nary_tuple]
NaryTupleMap.f [variable, in CoqApprox.nary_tuple]
NaryTupleMap.rT [variable, in CoqApprox.nary_tuple]
NaryTupleMap.T [variable, in CoqApprox.nary_tuple]
NaryTupleMk [section, in CoqApprox.nary_tuple]
NaryTupleMkNat [section, in CoqApprox.nary_tuple]
NaryTupleMkNat.f [variable, in CoqApprox.nary_tuple]
NaryTupleMkNat.n [variable, in CoqApprox.nary_tuple]
NaryTupleMkNat.U [variable, in CoqApprox.nary_tuple]
NaryTupleMk.f [variable, in CoqApprox.nary_tuple]
NaryTupleMk.n [variable, in CoqApprox.nary_tuple]
NaryTupleMk.U [variable, in CoqApprox.nary_tuple]
NaryTupleSeq [section, in CoqApprox.nary_tuple]
NaryTupleSeq.n [variable, in CoqApprox.nary_tuple]
NaryTupleSeq.T [variable, in CoqApprox.nary_tuple]
NaryTuple.n [variable, in CoqApprox.nary_tuple]
NaryTuple.T [variable, in CoqApprox.nary_tuple]
NaryTuple1 [section, in CoqApprox.nary_tuple]
NaryTuple1.n [variable, in CoqApprox.nary_tuple]
NaryTuple1.T [variable, in CoqApprox.nary_tuple]
nary_tuple [library]
NatCompl [section, in CoqApprox.seq_compl]
nat_ind_gen [lemma, in CoqApprox.seq_compl]
NDerive [section, in CoqApprox.xreal_ssr_compat]
NDerive.dom [variable, in CoqApprox.xreal_ssr_compat]
NDerive.Hder [variable, in CoqApprox.xreal_ssr_compat]
NDerive.Hdif [variable, in CoqApprox.xreal_ssr_compat]
NDerive.Hdom [variable, in CoqApprox.xreal_ssr_compat]
NDerive.n [variable, in CoqApprox.xreal_ssr_compat]
NDerive.X [variable, in CoqApprox.xreal_ssr_compat]
NDerive.XD [variable, in CoqApprox.xreal_ssr_compat]
NDerive.XD0_Xnan [variable, in CoqApprox.xreal_ssr_compat]
not_Xnan_Xreal_fun [lemma, in CoqApprox.xreal_ssr_compat]
nseq_Tuple [definition, in CoqApprox.nary_tuple]
nth_recNup_indep [lemma, in CoqApprox.basic_rec]
nth_recNdown_indep [lemma, in CoqApprox.basic_rec]
nth_recNdown_dflt2 [lemma, in CoqApprox.basic_rec]
nth_recNdown [lemma, in CoqApprox.basic_rec]
nth_rec2up_indep [lemma, in CoqApprox.basic_rec]
nth_rec2down_indep [lemma, in CoqApprox.basic_rec]
nth_rec2down_dflt2 [lemma, in CoqApprox.basic_rec]
nth_rec2down [lemma, in CoqApprox.basic_rec]
nth_rec1down_dflt2 [lemma, in CoqApprox.basic_rec]
nth_rec1down [lemma, in CoqApprox.basic_rec]
nth_defaults [lemma, in CoqApprox.basic_rec]
nth_mkTuple [lemma, in CoqApprox.nary_tuple]
nth_mkTupleO [lemma, in CoqApprox.nary_tuple]
nth_Xderive_pt_var [lemma, in CoqApprox.derive_compl]
nth_Xderive_pt_cst [lemma, in CoqApprox.derive_compl]
nth_Xderive_pt_cos [lemma, in CoqApprox.derive_compl]
nth_derivable_pt_cos [lemma, in CoqApprox.derive_compl]
nth_Xderive_pt_sin [lemma, in CoqApprox.derive_compl]
nth_Xcos [definition, in CoqApprox.derive_compl]
nth_Xsin [definition, in CoqApprox.derive_compl]
nth_derivable_pt_sin [lemma, in CoqApprox.derive_compl]
nth_Xderive_pt_invsqrt [lemma, in CoqApprox.derive_compl]
nth_Xderive_pt_sqrt [lemma, in CoqApprox.derive_compl]
nth_derivable_pt_sqrt [lemma, in CoqApprox.derive_compl]
nth_derivable_pt_power [lemma, in CoqApprox.derive_compl]
nth_Xderive_pt_inv [lemma, in CoqApprox.derive_compl]
nth_derivable_pt_inv [lemma, in CoqApprox.derive_compl]
nth_derivable_pt_inv_pow [lemma, in CoqApprox.derive_compl]
nth_Xderive_pt_pow [lemma, in CoqApprox.derive_compl]
nth_derivable_pt_pow [lemma, in CoqApprox.derive_compl]
nth_pow [section, in CoqApprox.derive_compl]
nth_Xderive_pt_exp [lemma, in CoqApprox.derive_compl]
nth_derivable_pt_exp [lemma, in CoqApprox.derive_compl]
nth_exp [section, in CoqApprox.derive_compl]
nth_Xderive_pt [definition, in CoqApprox.derive_compl]
nth_derivable_pt [definition, in CoqApprox.derive_compl]
nth_map2 [lemma, in CoqApprox.seq_compl]
nth1 [lemma, in CoqApprox.seq_compl]
nuncurry_ncurry [lemma, in CoqApprox.basic_rec]
nuncurry_const [lemma, in CoqApprox.basic_rec]
nuncurry2 [definition, in CoqApprox.coeff_inst]


O

Oab [abbreviation, in CoqApprox.taylor_thm]
ordinal1 [lemma, in CoqApprox.xreal_ssr_compat]
ord_Tuple [definition, in CoqApprox.nary_tuple]


P

pickR [definition, in CoqApprox.Rstruct]
pickR_ext [lemma, in CoqApprox.Rstruct]
pickR_ex [lemma, in CoqApprox.Rstruct]
pickR_some [lemma, in CoqApprox.Rstruct]
PolF [module, in CoqApprox.test_exp_sin]
PolI [module, in CoqApprox.test_exp_sin]
PolX [module, in CoqApprox.test_exp_sin]
PolyMap [module, in CoqApprox.taylor_model_float_sharp]
PolyMap.tnth_polymap [lemma, in CoqApprox.taylor_model_float_sharp]
PolyMap.tpolymap [definition, in CoqApprox.taylor_model_float_sharp]
PolyMap.tpolymap_polyNil [definition, in CoqApprox.taylor_model_float_sharp]
PolyMap.tpolymap_polyCons [definition, in CoqApprox.taylor_model_float_sharp]
PolyMap.tsize_polymap [lemma, in CoqApprox.taylor_model_float_sharp]
PolyOps [module, in CoqApprox.poly_datatypes]
PolyOps.teval [axiom, in CoqApprox.poly_datatypes]
PolyOps.tfold [axiom, in CoqApprox.poly_datatypes]
PolyOps.tfold_polyCons [axiom, in CoqApprox.poly_datatypes]
PolyOps.tfold_polyNil [axiom, in CoqApprox.poly_datatypes]
PolyOps.tlastN [axiom, in CoqApprox.poly_datatypes]
PolyOps.tlastN_spec [axiom, in CoqApprox.poly_datatypes]
PolyOps.tmul_tail [axiom, in CoqApprox.poly_datatypes]
PolyOps.tmul_trunc [axiom, in CoqApprox.poly_datatypes]
PolyOps.tnth [axiom, in CoqApprox.poly_datatypes]
PolyOps.tnth_set_nth_neq [axiom, in CoqApprox.poly_datatypes]
PolyOps.tnth_set_nth_eq [axiom, in CoqApprox.poly_datatypes]
PolyOps.tnth_out [axiom, in CoqApprox.poly_datatypes]
PolyOps.tnth_polyNil [axiom, in CoqApprox.poly_datatypes]
PolyOps.tnth_polyCons [axiom, in CoqApprox.poly_datatypes]
PolyOps.tnth_tadd [axiom, in CoqApprox.poly_datatypes]
PolyOps.tpolyCons [axiom, in CoqApprox.poly_datatypes]
PolyOps.tpolyNil [axiom, in CoqApprox.poly_datatypes]
PolyOps.tpoly_ind [axiom, in CoqApprox.poly_datatypes]
PolyOps.trecN [axiom, in CoqApprox.poly_datatypes]
PolyOps.trecN_spec [axiom, in CoqApprox.poly_datatypes]
PolyOps.trecN_spec0 [axiom, in CoqApprox.poly_datatypes]
PolyOps.trec1 [axiom, in CoqApprox.poly_datatypes]
PolyOps.trec1_spec [axiom, in CoqApprox.poly_datatypes]
PolyOps.trec1_spec0 [axiom, in CoqApprox.poly_datatypes]
PolyOps.trec2 [axiom, in CoqApprox.poly_datatypes]
PolyOps.trec2_spec [axiom, in CoqApprox.poly_datatypes]
PolyOps.trec2_spec1 [axiom, in CoqApprox.poly_datatypes]
PolyOps.trec2_spec0 [axiom, in CoqApprox.poly_datatypes]
PolyOps.tset_nth [axiom, in CoqApprox.poly_datatypes]
PolyOps.tsize [axiom, in CoqApprox.poly_datatypes]
PolyOps.tsize_set_nth [axiom, in CoqApprox.poly_datatypes]
PolyOps.tsize_polyNil [axiom, in CoqApprox.poly_datatypes]
PolyOps.tsize_polyCons [axiom, in CoqApprox.poly_datatypes]
PolyOps.tsize_tadd [axiom, in CoqApprox.poly_datatypes]
PolyOps.tsize_mul_tail [axiom, in CoqApprox.poly_datatypes]
PolyOps.tsize_mul_trunc [axiom, in CoqApprox.poly_datatypes]
PolyOps.tsize_trec2 [axiom, in CoqApprox.poly_datatypes]
PolyOps.tsize_trec1 [axiom, in CoqApprox.poly_datatypes]
PolyOps.tsize_trecN [axiom, in CoqApprox.poly_datatypes]
poly_inst_seq [library]
poly_datatypes [library]
PowDivOps [module, in CoqApprox.poly_datatypes]
PowDivOps0 [module, in CoqApprox.poly_datatypes]
power [section, in CoqApprox.derive_compl]
predn_leq [lemma, in CoqApprox.seq_compl]
ProofN [section, in CoqApprox.basic_rec]
ProofN' [section, in CoqApprox.basic_rec]
ProofN.F [variable, in CoqApprox.basic_rec]
ProofN.init [variable, in CoqApprox.basic_rec]
ProofN.N [variable, in CoqApprox.basic_rec]
ProofN.T [variable, in CoqApprox.basic_rec]


R

Radd_add_law [definition, in CoqApprox.Rstruct]
Radd_comoid [definition, in CoqApprox.Rstruct]
Radd_monoid [definition, in CoqApprox.Rstruct]
real_field [definition, in CoqApprox.Rstruct]
real_fieldIdomainMixin [definition, in CoqApprox.Rstruct]
real_fieldMixin [lemma, in CoqApprox.Rstruct]
real_idomainType [definition, in CoqApprox.Rstruct]
real_idomainMixin [lemma, in CoqApprox.Rstruct]
real_comUnitRingType [definition, in CoqApprox.Rstruct]
real_unitRing [definition, in CoqApprox.Rstruct]
real_unitRingMixin [definition, in CoqApprox.Rstruct]
real_comringType [definition, in CoqApprox.Rstruct]
real_ringType [definition, in CoqApprox.Rstruct]
real_ringMixin [definition, in CoqApprox.Rstruct]
real_zmodType [definition, in CoqApprox.Rstruct]
real_zmodMixin [definition, in CoqApprox.Rstruct]
real_eqType [definition, in CoqApprox.Rstruct]
real_eqMixin [definition, in CoqApprox.Rstruct]
recNdown [definition, in CoqApprox.basic_rec]
recNdownE [lemma, in CoqApprox.basic_rec]
recNdown_correct [lemma, in CoqApprox.basic_rec]
recNdown_init_correct [lemma, in CoqApprox.basic_rec]
recNup [definition, in CoqApprox.basic_rec]
recNup_correct [lemma, in CoqApprox.basic_rec]
recNup_init_correct [lemma, in CoqApprox.basic_rec]
rec1down [definition, in CoqApprox.basic_rec]
rec1down_co0' [lemma, in CoqApprox.basic_rec]
rec1down_co0 [lemma, in CoqApprox.basic_rec]
rec1down_nth_indep [lemma, in CoqApprox.basic_rec]
rec1down_correct [lemma, in CoqApprox.basic_rec]
rec1up [definition, in CoqApprox.basic_rec]
rec1up_co0' [lemma, in CoqApprox.basic_rec]
rec1up_co0 [lemma, in CoqApprox.basic_rec]
rec1up_nth_indep [lemma, in CoqApprox.basic_rec]
rec1up_correct [lemma, in CoqApprox.basic_rec]
rec1up_nth_last [lemma, in CoqApprox.basic_rec]
rec2down [definition, in CoqApprox.basic_rec]
rec2down_co1 [lemma, in CoqApprox.basic_rec]
rec2down_co0 [lemma, in CoqApprox.basic_rec]
rec2down_correct' [lemma, in CoqApprox.basic_rec]
rec2down_correct [lemma, in CoqApprox.basic_rec]
rec2up [definition, in CoqApprox.basic_rec]
rec2up_co1 [lemma, in CoqApprox.basic_rec]
rec2up_co0 [lemma, in CoqApprox.basic_rec]
rec2up_correct' [lemma, in CoqApprox.basic_rec]
rec2up_correct [lemma, in CoqApprox.basic_rec]
rec2up_nth_last [lemma, in CoqApprox.basic_rec]
Req_EM_T [lemma, in CoqApprox.Rstruct]
rev_iota [lemma, in CoqApprox.poly_inst_seq]
rev' [definition, in CoqApprox.basic_rec]
rev'E [lemma, in CoqApprox.basic_rec]
Rgeb [definition, in CoqApprox.Rstruct]
RgeP [lemma, in CoqApprox.Rstruct]
Rgtb [definition, in CoqApprox.Rstruct]
RgtP [lemma, in CoqApprox.Rstruct]
right_distr_Rmult_Rplus [lemma, in CoqApprox.xreal_ssr_compat]
RigPolyApprox [module, in CoqApprox.poly_datatypes]
RigPolyApproxFloat [module, in CoqApprox.taylor_model_float_sharp]
RigPolyApproxFloat.Fl [module, in CoqApprox.taylor_model_float_sharp]
RigPolyApproxInt [module, in CoqApprox.rpa_inst]
RigPolyApprox.approx [projection, in CoqApprox.poly_datatypes]
RigPolyApprox.error [projection, in CoqApprox.poly_datatypes]
RigPolyApprox.rpa [record, in CoqApprox.poly_datatypes]
RigPolyApprox.RPA [constructor, in CoqApprox.poly_datatypes]
Rinvx [definition, in CoqApprox.Rstruct]
RinvxRmult [lemma, in CoqApprox.Rstruct]
Rinvx_out [lemma, in CoqApprox.Rstruct]
Rleb [definition, in CoqApprox.Rstruct]
RleP [lemma, in CoqApprox.Rstruct]
Rltb [definition, in CoqApprox.Rstruct]
RltP [lemma, in CoqApprox.Rstruct]
rmlast [definition, in CoqApprox.seq_compl]
rmlast_cons [lemma, in CoqApprox.seq_compl]
RmultA [lemma, in CoqApprox.Rstruct]
RmultRinvx [lemma, in CoqApprox.Rstruct]
Rmul_mul_law [definition, in CoqApprox.Rstruct]
Rmul_comoid [definition, in CoqApprox.Rstruct]
Rmul_monoid [definition, in CoqApprox.Rstruct]
Rneq_lt [lemma, in CoqApprox.xreal_ssr_compat]
Rolle_lim [lemma, in CoqApprox.taylor_thm]
rpa_inst [library]
RplusA [lemma, in CoqApprox.Rstruct]
Rstruct [library]
R_choiceType [definition, in CoqApprox.Rstruct]
R_choiceMixin [definition, in CoqApprox.Rstruct]
R1_neq_0 [lemma, in CoqApprox.Rstruct]


S

SeqPolyMonomUp [module, in CoqApprox.poly_inst_seq]
SeqPolyMonomUpFloat [module, in CoqApprox.poly_inst_seq]
SeqPolyMonomUpFloat.Fl [module, in CoqApprox.poly_inst_seq]
SeqPolyMonomUpInt [module, in CoqApprox.poly_inst_seq]
SeqPolyMonomUpInt.Int [module, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.mul_coeffE' [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.mul_coeff [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.PrecIsPropagated [section, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.PrecIsPropagated.u [variable, in CoqApprox.poly_inst_seq]
_ * _ [notation, in CoqApprox.poly_inst_seq]
_ + _ [notation, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.size_tsub [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.size_topp [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.T [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tadd [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.teval [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.teval_polyCons [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.teval_polyNil [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tfold [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tfold_polyCons [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tfold_polyNil [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tlastN [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tlastN_spec [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tmap [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tmul [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tmul_tail [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tmul_trunc [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_out [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_set_nth_neq [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_set_nth_eq [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_polyNil [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_polyCons [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_tadd [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_map [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tone [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.topp [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tpolyCons [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tpolyNil [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tpoly_ind [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trecN [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trecN_spec [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trecN_spec0 [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec1 [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec1_spec [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec1_spec0 [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec2 [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec2_spec [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec2_spec1 [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec2_spec0 [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tset_nth [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_set_nth [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_mul_tail [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_mul_trunc [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_polyNil [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_polyCons [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_trecN [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_trec2 [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_trec1 [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_tadd [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_map [lemma, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsub [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tzero [definition, in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.U [definition, in CoqApprox.poly_inst_seq]
seq_compl [library]
sin_cos [section, in CoqApprox.derive_compl]
size_recNup [lemma, in CoqApprox.basic_rec]
size_recNdown [lemma, in CoqApprox.basic_rec]
size_loopN [lemma, in CoqApprox.basic_rec]
size_rec2up [lemma, in CoqApprox.basic_rec]
size_rec2down [lemma, in CoqApprox.basic_rec]
size_loop2 [lemma, in CoqApprox.basic_rec]
size_rec1up [lemma, in CoqApprox.basic_rec]
size_rec1down [lemma, in CoqApprox.basic_rec]
size_loop1 [lemma, in CoqApprox.basic_rec]
size_Tuple [lemma, in CoqApprox.nary_tuple]
size_map2 [lemma, in CoqApprox.seq_compl]
size_take_minn [lemma, in CoqApprox.seq_compl]
SliceExactBaseOps [module, in CoqApprox.poly_datatypes]
SliceExactBaseOps.big_distrr_spec [axiom, in CoqApprox.poly_datatypes]
SliceExactBaseOps.tadd_assoc [axiom, in CoqApprox.poly_datatypes]
SliceExactBaseOps.tadd_comm [axiom, in CoqApprox.poly_datatypes]
SliceExactBaseOps.tadd_zeror [axiom, in CoqApprox.poly_datatypes]
SliceExactBaseOps.tadd_zerol [axiom, in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_distrr [axiom, in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_distrl [axiom, in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_assoc [axiom, in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_comm [axiom, in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_oner [axiom, in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_onel [axiom, in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps [module, in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_comm [axiom, in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_idemp [axiom, in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_mul_r [axiom, in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_mul_l [axiom, in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_add_r [axiom, in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_add_l [axiom, in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask0mul_r [axiom, in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask0mul_l [axiom, in CoqApprox.poly_datatypes]
SliceExactMonomPolyOps [module, in CoqApprox.poly_datatypes]
SliceExactMonomPolyOps.Ctpow [abbreviation, in CoqApprox.poly_datatypes]
SliceExactMonomPolyOps.is_horner [axiom, in CoqApprox.poly_datatypes]
SliceExactMonomPolyOps.tmul_tail_nth [axiom, in CoqApprox.poly_datatypes]
SliceExactMonomPolyOps.tmul_trunc_nth [axiom, in CoqApprox.poly_datatypes]
SliceExactPowDivOps [module, in CoqApprox.poly_datatypes]
SliceExactPowDivOps.tpow [abbreviation, in CoqApprox.poly_datatypes]
SliceExactPowDivOps.tpow_opp [axiom, in CoqApprox.poly_datatypes]
SliceExactPowDivOps.tpow_S [axiom, in CoqApprox.poly_datatypes]
SliceExactPowDivOps.tpow_0 [axiom, in CoqApprox.poly_datatypes]
SliceFullOps [module, in CoqApprox.poly_datatypes]
SliceFullOps.tcos [axiom, in CoqApprox.poly_datatypes]
SliceFullOps.texp [axiom, in CoqApprox.poly_datatypes]
SliceFullOps.tinvsqrt [axiom, in CoqApprox.poly_datatypes]
SliceFullOps.tnat [axiom, in CoqApprox.poly_datatypes]
SliceFullOps.tsin [axiom, in CoqApprox.poly_datatypes]
SliceFullOps.tsqrt [axiom, in CoqApprox.poly_datatypes]
SliceMaskBaseOps [module, in CoqApprox.poly_datatypes]
SliceMaskBaseOps.tcst [axiom, in CoqApprox.poly_datatypes]
SliceMonomPolyOps [module, in CoqApprox.poly_datatypes]
SliceMonomPolyOps.teval_polyNil [axiom, in CoqApprox.poly_datatypes]
SliceMonomPolyOps.teval_polyCons [axiom, in CoqApprox.poly_datatypes]
SlicePowDivOps [module, in CoqApprox.poly_datatypes]
SlicePowDivOps.tdiv [axiom, in CoqApprox.poly_datatypes]
SlicePowDivOps.tinv [axiom, in CoqApprox.poly_datatypes]
SlicePowDivOps.tpower_int [axiom, in CoqApprox.poly_datatypes]
SlicePowDivOps.tsqr [axiom, in CoqApprox.poly_datatypes]
slideN [definition, in CoqApprox.basic_rec]
slideN_lastN [lemma, in CoqApprox.basic_rec]
slideN_aux [definition, in CoqApprox.basic_rec]
snd' [definition, in CoqApprox.basic_rec]
square_root [section, in CoqApprox.derive_compl]
subset_refl [lemma, in CoqApprox.interval_compl]
subset_ [abbreviation, in CoqApprox.interval_compl]
sum_f_to_big [lemma, in CoqApprox.xreal_ssr_compat]


T

Take [section, in CoqApprox.seq_compl]
takeN [definition, in CoqApprox.nary_tuple]
takeN_Ttoseq [lemma, in CoqApprox.nary_tuple]
takeN_lastN.d [variable, in CoqApprox.nary_tuple]
takeN_lastN.T [variable, in CoqApprox.nary_tuple]
takeN_lastN [section, in CoqApprox.nary_tuple]
take_drop_rev [lemma, in CoqApprox.nary_tuple]
Take.T [variable, in CoqApprox.seq_compl]
TaylorLagrange [section, in CoqApprox.taylor_thm]
TaylorLagrange.a [variable, in CoqApprox.taylor_thm]
TaylorLagrange.b [variable, in CoqApprox.taylor_thm]
TaylorLagrange.CorTL [section, in CoqApprox.taylor_thm]
TaylorLagrange.CorTL.derivable_pt_lim_Dp [variable, in CoqApprox.taylor_thm]
TaylorLagrange.D [variable, in CoqApprox.taylor_thm]
TaylorLagrange.n [variable, in CoqApprox.taylor_thm]
TaylorLagrange.TL [section, in CoqApprox.taylor_thm]
TaylorLagrange.TL.c [variable, in CoqApprox.taylor_thm]
TaylorLagrange.TL.continuity_pt_Dp [variable, in CoqApprox.taylor_thm]
TaylorLagrange.TL.derivable_pt_lim_Dp [variable, in CoqApprox.taylor_thm]
TaylorLagrange.TL.g [variable, in CoqApprox.taylor_thm]
TaylorLagrange.TL.Hx [variable, in CoqApprox.taylor_thm]
TaylorLagrange.TL.Hx0 [variable, in CoqApprox.taylor_thm]
TaylorLagrange.TL.x [variable, in CoqApprox.taylor_thm]
TaylorLagrange.TL.x0 [variable, in CoqApprox.taylor_thm]
TaylorModel [module, in CoqApprox.taylor_model_int_sharp]
TaylorModelFloat [module, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.contains_bnd2 [lemma, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_validTM [definition, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_approx [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_error [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_RPA [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_rpa [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_poly [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_type [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f2i [definition, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f2x [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f2x_poly [definition, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.Imask_mask [lemma, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_poly_map [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_eval [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_prec [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_approx [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_error [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_RPA [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_rpa [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_poly [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_type [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_tm_correct [lemma, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_mid_nan [lemma, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_tm [definition, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_rem [definition, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_poly [definition, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_mid_correct [lemma, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_mid [definition, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2ix [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.MapFX [module, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.MapI [module, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.MapIF [module, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.RPAF [module, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.subset_ [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.sub_midp_contains_0 [lemma, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.teval_contains_0 [lemma, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.TM [module, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.Xsub_diag_eq [lemma, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.Xsub_Xnan_r [lemma, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.x_eval [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.x_poly [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.x_type [abbreviation, in CoqApprox.taylor_model_float_sharp]
TaylorModel.bigXadd_real [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd_XP [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd_Si [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd_ni [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd_nS [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd'_real [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd'_XP [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd'_real_S [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd'_XP_S [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_contains_upper [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_contains_lower [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_upper_Xnan [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_lower_Xnan [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_Iupper [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_Ilower [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_IIbnd [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_IInan [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_singleton_contains_lower_upper [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Compat_rec2 [projection, in CoqApprox.taylor_model_int_sharp]
TaylorModel.compat_rec2 [record, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Compat_rec2 [constructor, in CoqApprox.taylor_model_int_sharp]
TaylorModel.compat_rec2 [inductive, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Compat_rec1 [projection, in CoqApprox.taylor_model_int_sharp]
TaylorModel.compat_rec1 [record, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Compat_rec1 [constructor, in CoqApprox.taylor_model_int_sharp]
TaylorModel.compat_rec1 [inductive, in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_IIbnd [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_Xgt [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_lower_or_upper [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_lower_or_upper_Xreal [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_IIbnd_Xreal [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_lower_le_upper [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.convert_teval [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.derivable_pt_lim_pow_sub [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.eq_Xcst_sign [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.eq'_Xcst_sign [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Extension2N [projection, in CoqApprox.taylor_model_int_sharp]
TaylorModel.extension2N [record, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Extension2N [constructor, in CoqApprox.taylor_model_int_sharp]
TaylorModel.extension2N [inductive, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Extension3N [projection, in CoqApprox.taylor_model_int_sharp]
TaylorModel.extension3N [record, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Extension3N [constructor, in CoqApprox.taylor_model_int_sharp]
TaylorModel.extension3N [inductive, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iadd_Isub_aux [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iadd_zero_subset_r [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iadd_zero_subset_l [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iadd_Inan_propagate_r [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iadd_Inan_propagate_l [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ibnd2 [abbreviation, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ilower_Xreal [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ilower_bnd [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Imul_Inan_propagate_r [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Imul_Inan_propagate_l [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.in_poly_bound [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ipow_Inan_propagate [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.IP_rec2 [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.IP_rec1 [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.isNNegOrNPos [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.isNNegOrNPos_false [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Isub_Inan_propagate_r [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Isub_Inan_propagate_l [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.is_horner_mask [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.is_horner_pos [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iupper_Xreal [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iupper_bnd [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.i_validTM_Ztech [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.i_validTM_TLrem [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.i_validTM_subset_X0 [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.i_validTM [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.le_lower_or [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.le_upper_or [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.lower_odd_Xneg_over [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.lower_odd_Xpos_over [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.lower_even_Xneg_over [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.lower_even_Xpos_over [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.lower_le [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.mul_error [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.mul_0_contains_0_r [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.mul_0_contains_0_l [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.notIInan_IIbnd [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.not_and_impl [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Nth_Xderive [projection, in CoqApprox.taylor_model_int_sharp]
TaylorModel.nth_Xderive [record, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Nth_Xderive [constructor, in CoqApprox.taylor_model_int_sharp]
TaylorModel.nth_Xderive [inductive, in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_eval_tm_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_eval_tm_correct_aux [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_eval_tm_correct_gen [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_eval_tm_correct_aux_gen [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_eval_tm [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_mul [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Poly_size' [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Poly_nth [projection, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Poly_size [projection, in CoqApprox.taylor_model_int_sharp]
TaylorModel.powerRZ_1_even [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.powerRZ_pow [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.pow_Rabs_sign [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.pow_contains_0 [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument [section, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.prec [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec [section, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.Corollaries [section, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.F0 [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.F0_contains [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.GenericProof [section, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.GenericProof.IP [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.GenericProof.XP [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec1_correct.F_rec [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec1_correct.XF_rec [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec1_correct [section, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.F_rec [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.XF_rec [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.F1_contains [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.XDn_1 [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.F1 [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.XF1 [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct [section, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.XDn [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.XF0 [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.XF0_Xnan [variable, in CoqApprox.taylor_model_int_sharp]
_ - _ [notation, in CoqApprox.taylor_model_int_sharp]
_ + _ [notation, in CoqApprox.taylor_model_int_sharp]
TaylorModel.proj_fun_id [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_1_r [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_twice [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_neg_compat_rev [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_neg_compat [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_pos_compat_rev [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_pos_compat [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rlt_neq_sym [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rlt_neq [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ropp_le_0 [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.RPA [module, in CoqApprox.taylor_model_int_sharp]
TaylorModel.size_poly_eval_tm [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.size_TM_mul [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.size_TM_add [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.subset_real_contains [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.subset_sub_contains_0 [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TaylorModel [section, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TaylorModel.M [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TaylorModel.prec [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TaylorModel.Tcoeffs [variable, in CoqApprox.taylor_model_int_sharp]
TaylorModel.teval_poly_nan [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.teval_in_nan [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.teval_contains [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TI [module, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TLrem [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TMset0 [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TMset0_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_div_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_div [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_inv_comp_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_inv_comp [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_comp_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_comp [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_type [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_fun_eq [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_mul_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_mul_correct_gen [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_mul [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_add_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_add_correct_gen [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_cos_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_sin_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_invsqrt_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_sqrt_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_exp_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_inv_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_var_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_cst_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_rec2_correct' [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_rec2_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_rec1_correct' [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_rec1_correct [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_add [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_cos [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_sin [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_invsqrt [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_sqrt [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_exp [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_inv [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_var [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_cst [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.tpolyNil_size0 [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.TX [module, in CoqApprox.taylor_model_int_sharp]
TaylorModel.upper_Xneg_over [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.upper_Xpos_over [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.upper_le [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.validPoly [record, in CoqApprox.taylor_model_int_sharp]
TaylorModel.ValidPoly [constructor, in CoqApprox.taylor_model_int_sharp]
TaylorModel.validPoly_rec2 [instance, in CoqApprox.taylor_model_int_sharp]
TaylorModel.validPoly_rec1 [instance, in CoqApprox.taylor_model_int_sharp]
TaylorModel.validXPoly [record, in CoqApprox.taylor_model_int_sharp]
TaylorModel.ValidXPoly [constructor, in CoqApprox.taylor_model_int_sharp]
TaylorModel.validXPoly_rec2 [instance, in CoqApprox.taylor_model_int_sharp]
TaylorModel.validXPoly_rec1 [instance, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xcmp_lt_imp_fun [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xcmp_gt_imp_fun [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xcmp_same [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xcst_sign [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdecr [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta_real [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta_idem' [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta_idem [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta_mask [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta_big [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta'_real [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta'_big [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xder [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_delta [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_pt_sub_r [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_pt_sub' [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_cst_sign [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_neg_imp_decr [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_pos_imp_incr [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_over_propagate' [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_over_propagate [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_over [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdiv_1_r [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.XDn_Xnan' [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.XDn_Xnan [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.XDn_0 [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xeq_imp [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xincr [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xmonot [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xmonot_contains_weak [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xmonot_contains [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xnan_ex_S [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xnan_ex_not [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xnan_ex_or [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xnan_ex [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xneg_Xadd [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xneg_over [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.XPoly_nth0 [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.XPoly_nth [projection, in CoqApprox.taylor_model_int_sharp]
TaylorModel.XPoly_size [projection, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xpos_over [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.XP_rec2 [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.XP_rec1 [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xreal_over_imp [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xreal_over' [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xreal_over [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xsub_0_r [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xund_contra [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xund_imp [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.ZEven_pow_le [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.ZOdd_pow_le [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ztech [definition, in CoqApprox.taylor_model_int_sharp]
TaylorModel.ZtechE1 [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.ZtechE2 [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ztech_derive_sign [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorModel.Zumkeller_monot_rem [lemma, in CoqApprox.taylor_model_int_sharp]
TaylorPoly [module, in CoqApprox.taylor_poly]
TaylorPolyOps [module, in CoqApprox.taylor_poly]
TaylorPolyOps.T_invsqrt [axiom, in CoqApprox.taylor_poly]
TaylorPolyOps.T_sqrt [axiom, in CoqApprox.taylor_poly]
TaylorPolyOps.T_cos [axiom, in CoqApprox.taylor_poly]
TaylorPolyOps.T_sin [axiom, in CoqApprox.taylor_poly]
TaylorPolyOps.T_exp [axiom, in CoqApprox.taylor_poly]
TaylorPolyOps.T_inv [axiom, in CoqApprox.taylor_poly]
TaylorPolyOps.T_var [axiom, in CoqApprox.taylor_poly]
TaylorPolyOps.T_cst [axiom, in CoqApprox.taylor_poly]
TaylorPoly.PrecIsPropagated [section, in CoqApprox.taylor_poly]
TaylorPoly.PrecIsPropagated.u [variable, in CoqApprox.taylor_poly]
TaylorPoly.Rec [module, in CoqApprox.taylor_poly]
TaylorPoly.T_invsqrt [definition, in CoqApprox.taylor_poly]
TaylorPoly.T_sqrt [definition, in CoqApprox.taylor_poly]
TaylorPoly.T_cos [definition, in CoqApprox.taylor_poly]
TaylorPoly.T_sin [definition, in CoqApprox.taylor_poly]
TaylorPoly.T_exp [definition, in CoqApprox.taylor_poly]
TaylorPoly.T_inv [definition, in CoqApprox.taylor_poly]
TaylorPoly.T_var [definition, in CoqApprox.taylor_poly]
TaylorPoly.T_cst [definition, in CoqApprox.taylor_poly]
TaylorRec [module, in CoqApprox.taylor_poly]
TaylorRec.cos_rec [definition, in CoqApprox.taylor_poly]
TaylorRec.cst_rec [definition, in CoqApprox.taylor_poly]
TaylorRec.exp_rec [definition, in CoqApprox.taylor_poly]
TaylorRec.invsqrt_rec [definition, in CoqApprox.taylor_poly]
TaylorRec.inv_rec [definition, in CoqApprox.taylor_poly]
TaylorRec.PrecIsPropagated [section, in CoqApprox.taylor_poly]
TaylorRec.PrecIsPropagated.u [variable, in CoqApprox.taylor_poly]
_ / _ [notation, in CoqApprox.taylor_poly]
_ * _ [notation, in CoqApprox.taylor_poly]
_ - _ [notation, in CoqApprox.taylor_poly]
_ + _ [notation, in CoqApprox.taylor_poly]
TaylorRec.sin_rec [definition, in CoqApprox.taylor_poly]
TaylorRec.sqrt_rec [definition, in CoqApprox.taylor_poly]
TaylorRec.var_rec [definition, in CoqApprox.taylor_poly]
Taylor_Lagrange [lemma, in CoqApprox.taylor_thm]
taylor_poly [library]
taylor_model_float_sharp [library]
taylor_model_int_sharp [library]
taylor_thm [library]
Tcast [definition, in CoqApprox.nary_tuple]
TcastE [lemma, in CoqApprox.nary_tuple]
TcastK [lemma, in CoqApprox.nary_tuple]
TcastKV [lemma, in CoqApprox.nary_tuple]
Tcast_trans [lemma, in CoqApprox.nary_tuple]
Tcast_id [lemma, in CoqApprox.nary_tuple]
Tcoeff [abbreviation, in CoqApprox.taylor_thm]
TestN [section, in CoqApprox.basic_rec]
TestN.F [variable, in CoqApprox.basic_rec]
TestN.FibN [variable, in CoqApprox.basic_rec]
TestN.FibNc [variable, in CoqApprox.basic_rec]
TestN.FibNc' [variable, in CoqApprox.basic_rec]
TestN.FibNs [variable, in CoqApprox.basic_rec]
TestN.FibNs' [variable, in CoqApprox.basic_rec]
TestN.FibN' [variable, in CoqApprox.basic_rec]
TestN.Fib2 [variable, in CoqApprox.basic_rec]
test_exp_sin [library]
Test1 [section, in CoqApprox.basic_rec]
Test1.fact [variable, in CoqApprox.basic_rec]
Test1.factz_rec [variable, in CoqApprox.basic_rec]
Test1.fact_rec [variable, in CoqApprox.basic_rec]
Test1.n_rec [variable, in CoqApprox.basic_rec]
Test2 [section, in CoqApprox.basic_rec]
Test2.fibz_rec [variable, in CoqApprox.basic_rec]
Test2.foo2 [variable, in CoqApprox.basic_rec]
Test2.foo2_rec [variable, in CoqApprox.basic_rec]
Thead [definition, in CoqApprox.nary_tuple]
TheadE [lemma, in CoqApprox.nary_tuple]
TMF [module, in CoqApprox.test_exp_sin]
TM_comp_0.tm' [definition, in CoqApprox.test_exp_sin]
TM_comp_0.tm [definition, in CoqApprox.test_exp_sin]
TM_comp_0.tm_sin [definition, in CoqApprox.test_exp_sin]
TM_comp_0.pr [definition, in CoqApprox.test_exp_sin]
TM_comp_0.deg [definition, in CoqApprox.test_exp_sin]
TM_comp_0.X0 [definition, in CoqApprox.test_exp_sin]
TM_comp_0.c [definition, in CoqApprox.test_exp_sin]
TM_comp_0.X [definition, in CoqApprox.test_exp_sin]
TM_comp_0.b [definition, in CoqApprox.test_exp_sin]
TM_comp_0.a [definition, in CoqApprox.test_exp_sin]
TM_comp_0 [module, in CoqApprox.test_exp_sin]
Tnth [definition, in CoqApprox.nary_tuple]
Tnth_lastN [lemma, in CoqApprox.nary_tuple]
Tnth_mkTuple [lemma, in CoqApprox.nary_tuple]
Tnth_mkTupleO [lemma, in CoqApprox.nary_tuple]
Tnth_ord_Tuple [lemma, in CoqApprox.nary_tuple]
Tnth_Tuplify [lemma, in CoqApprox.nary_tuple]
tnth_tuplify [lemma, in CoqApprox.nary_tuple]
Tnth_map_Tuple [lemma, in CoqApprox.nary_tuple]
Tnth_nth [lemma, in CoqApprox.nary_tuple]
Tnth_default [lemma, in CoqApprox.nary_tuple]
Tnth0 [lemma, in CoqApprox.nary_tuple]
Tofseq [definition, in CoqApprox.nary_tuple]
TofseqK [lemma, in CoqApprox.nary_tuple]
Tsize [definition, in CoqApprox.nary_tuple]
Tsum [abbreviation, in CoqApprox.taylor_thm]
Tterm [abbreviation, in CoqApprox.taylor_thm]
Ttoseq [definition, in CoqApprox.nary_tuple]
TtoseqK [lemma, in CoqApprox.nary_tuple]
Ttoseq_slideN [lemma, in CoqApprox.basic_rec]
Ttoseq_slideN_aux [lemma, in CoqApprox.basic_rec]
Ttoseq_lastN_rev' [lemma, in CoqApprox.nary_tuple]
Ttoseq_lastN_drop' [lemma, in CoqApprox.nary_tuple]
Ttoseq_lastN_rev [lemma, in CoqApprox.nary_tuple]
Ttoseq_lastN_drop [lemma, in CoqApprox.nary_tuple]
Ttoseq_takeN' [lemma, in CoqApprox.nary_tuple]
Ttoseq_takeN [lemma, in CoqApprox.nary_tuple]
Ttoseq_ord_Tuple [lemma, in CoqApprox.nary_tuple]
Ttoseq_Tuplify [lemma, in CoqApprox.nary_tuple]
Ttoseq_iota [lemma, in CoqApprox.nary_tuple]
Ttoseq_nseq [lemma, in CoqApprox.nary_tuple]
Ttoseq_map [lemma, in CoqApprox.nary_tuple]
Ttoseq_inj [lemma, in CoqApprox.nary_tuple]
Tuple_map_ord [lemma, in CoqApprox.nary_tuple]
Tuple0 [lemma, in CoqApprox.nary_tuple]
Tuple0eq [lemma, in CoqApprox.nary_tuple]
Tuplify [definition, in CoqApprox.nary_tuple]
tuplify [definition, in CoqApprox.nary_tuple]
Tuplify [section, in CoqApprox.nary_tuple]
TuplifyK [lemma, in CoqApprox.nary_tuple]
tuplifyK [lemma, in CoqApprox.nary_tuple]
Tuplify.T [variable, in CoqApprox.nary_tuple]


U

unit_R [definition, in CoqApprox.Rstruct]


V

val_tuplify [lemma, in CoqApprox.nary_tuple]


X

XaddA [lemma, in CoqApprox.xreal_ssr_compat]
XaddC [lemma, in CoqApprox.xreal_ssr_compat]
Xadd_comoid [definition, in CoqApprox.xreal_ssr_compat]
Xadd_monoid [definition, in CoqApprox.xreal_ssr_compat]
Xadd0 [lemma, in CoqApprox.xreal_ssr_compat]
Xderive_propagate' [lemma, in CoqApprox.xreal_ssr_compat]
Xderive_propagate [lemma, in CoqApprox.xreal_ssr_compat]
Xderive_pt_mulXmask [lemma, in CoqApprox.xreal_ssr_compat]
Xderive_pt_Xpow [lemma, in CoqApprox.xreal_ssr_compat]
Xderive_pt_mul_const [lemma, in CoqApprox.derive_compl]
XD_Xreal [lemma, in CoqApprox.xreal_ssr_compat]
XD_Xnan_propagate [lemma, in CoqApprox.xreal_ssr_compat]
Xinv_1 [lemma, in CoqApprox.xreal_ssr_compat]
XmulA [lemma, in CoqApprox.xreal_ssr_compat]
XmulC [lemma, in CoqApprox.xreal_ssr_compat]
Xmul_comoid [definition, in CoqApprox.xreal_ssr_compat]
Xmul_monoid [definition, in CoqApprox.xreal_ssr_compat]
Xmul_Xreal [lemma, in CoqApprox.xreal_ssr_compat]
Xmul0 [lemma, in CoqApprox.xreal_ssr_compat]
Xneg_as_Xmul [lemma, in CoqApprox.interval_compl]
Xpow [definition, in CoqApprox.xreal_ssr_compat]
Xpow_Xnan [lemma, in CoqApprox.xreal_ssr_compat]
Xpow_Xreal [lemma, in CoqApprox.xreal_ssr_compat]
Xpow_idem [lemma, in CoqApprox.xreal_ssr_compat]
Xpow_iter [definition, in CoqApprox.xreal_ssr_compat]
Xreal_irrelevance [lemma, in CoqApprox.xreal_ssr_compat]
Xreal_eqType [definition, in CoqApprox.xreal_ssr_compat]
Xreal_eqMixin [definition, in CoqApprox.xreal_ssr_compat]
xreal_ssr_compat [library]
XReq_EM_T [lemma, in CoqApprox.xreal_ssr_compat]
Xsub_Xnan_r [lemma, in CoqApprox.xreal_ssr_compat]
Xsub_Xreal_r [lemma, in CoqApprox.xreal_ssr_compat]
Xsub_Xreal_l [lemma, in CoqApprox.xreal_ssr_compat]
Xsub_Xadd_distr [lemma, in CoqApprox.xreal_ssr_compat]
XTaylor_Lagrange [lemma, in CoqApprox.xreal_ssr_compat]
X0add [lemma, in CoqApprox.xreal_ssr_compat]
X0mul [lemma, in CoqApprox.xreal_ssr_compat]


Z

zeroF [lemma, in CoqApprox.xreal_ssr_compat]
zeroT [lemma, in CoqApprox.xreal_ssr_compat]


other

[ Tuple _ | 0 <= _ < _ ] (form_scope) [notation, in CoqApprox.nary_tuple]
[ Tuple _ | _ < _ ] (form_scope) [notation, in CoqApprox.nary_tuple]
[ Tuple _ ; .. ; _ ] (form_scope) [notation, in CoqApprox.nary_tuple]
[ Tuple _ ] (form_scope) [notation, in CoqApprox.nary_tuple]
[ Tuple ] (form_scope) [notation, in CoqApprox.nary_tuple]
[ Tnth _ _ ] (form_scope) [notation, in CoqApprox.nary_tuple]
[ Tuple of _ ] (form_scope) [notation, in CoqApprox.nary_tuple]
_ ^ _ (XR_scope) [notation, in CoqApprox.xreal_ssr_compat]
_ / _ (XR_scope) [notation, in CoqApprox.xreal_ssr_compat]
_ * _ (XR_scope) [notation, in CoqApprox.xreal_ssr_compat]
- _ (XR_scope) [notation, in CoqApprox.xreal_ssr_compat]
_ - _ (XR_scope) [notation, in CoqApprox.xreal_ssr_compat]
_ + _ (XR_scope) [notation, in CoqApprox.xreal_ssr_compat]
_ *2^ _ [notation, in CoqApprox.test_exp_sin]



Instance Index

T

TaylorModel.validPoly_rec2 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.validPoly_rec1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.validXPoly_rec2 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.validXPoly_rec1 [in CoqApprox.taylor_model_int_sharp]



Projection Index

R

RigPolyApprox.approx [in CoqApprox.poly_datatypes]
RigPolyApprox.error [in CoqApprox.poly_datatypes]


T

TaylorModel.Compat_rec2 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Compat_rec1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Extension2N [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Extension3N [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Nth_Xderive [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Poly_nth [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Poly_size [in CoqApprox.taylor_model_int_sharp]
TaylorModel.XPoly_nth [in CoqApprox.taylor_model_int_sharp]
TaylorModel.XPoly_size [in CoqApprox.taylor_model_int_sharp]



Record Index

R

RigPolyApprox.rpa [in CoqApprox.poly_datatypes]


T

TaylorModel.compat_rec2 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.compat_rec1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.extension2N [in CoqApprox.taylor_model_int_sharp]
TaylorModel.extension3N [in CoqApprox.taylor_model_int_sharp]
TaylorModel.nth_Xderive [in CoqApprox.taylor_model_int_sharp]
TaylorModel.validPoly [in CoqApprox.taylor_model_int_sharp]
TaylorModel.validXPoly [in CoqApprox.taylor_model_int_sharp]



Lemma Index

B

behead_recNdown [in CoqApprox.basic_rec]
behead_rev_take [in CoqApprox.basic_rec]
behead_rcons [in CoqApprox.basic_rec]
behead_rec2down_again [in CoqApprox.basic_rec]
behead_rec2down [in CoqApprox.basic_rec]
behead_loop2 [in CoqApprox.basic_rec]
behead_rec1down [in CoqApprox.basic_rec]
bigXadd_bigRplus [in CoqApprox.xreal_ssr_compat]
bigXadd_Xreal_i [in CoqApprox.xreal_ssr_compat]
bigXadd_Xreal1 [in CoqApprox.xreal_ssr_compat]
bigXadd_Xreal [in CoqApprox.xreal_ssr_compat]
bigXadd_Xnan_i [in CoqApprox.xreal_ssr_compat]
bigXadd_Xnan [in CoqApprox.xreal_ssr_compat]
big_Xmul_Xadd_distr [in CoqApprox.xreal_ssr_compat]


C

contains_Xnan [in CoqApprox.xreal_ssr_compat]
contains_subset [in CoqApprox.interval_compl]
contains_trans [in CoqApprox.interval_compl]
continuity_pt_sum [in CoqApprox.taylor_thm]
continuity_pt_eq [in CoqApprox.taylor_thm]
Cor_Taylor_Lagrange [in CoqApprox.taylor_thm]


D

derivable_pt_lim_aux [in CoqApprox.taylor_thm]
derivable_pt_lim_sum [in CoqApprox.taylor_thm]


E

eqrP [in CoqApprox.Rstruct]
eqXP [in CoqApprox.xreal_ssr_compat]
eq_foldr [in CoqApprox.poly_inst_seq]
eq_from_Tnth [in CoqApprox.nary_tuple]
ExactSeqPolyMonomUp.is_horner [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.mask_big_helper [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.mul_coeffE [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.tmul_tail_nth [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.tmul_trunc_nth [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.trunc_leq [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.trunc_inc [in CoqApprox.poly_inst_seq]


F

fact_zeroF [in CoqApprox.xreal_ssr_compat]
foldl_cons0 [in CoqApprox.seq_compl]
foldl_cons [in CoqApprox.seq_compl]
foldr_cons0 [in CoqApprox.seq_compl]
foldr_cons [in CoqApprox.seq_compl]
FullInt.zero_correct [in CoqApprox.coeff_inst]
FullXR.big_distrr_spec [in CoqApprox.coeff_inst]
FullXR.mask_comm [in CoqApprox.coeff_inst]
FullXR.mask_idemp [in CoqApprox.coeff_inst]
FullXR.mask_mul_r [in CoqApprox.coeff_inst]
FullXR.mask_mul_l [in CoqApprox.coeff_inst]
FullXR.mask_add_r [in CoqApprox.coeff_inst]
FullXR.mask_add_l [in CoqApprox.coeff_inst]
FullXR.mask0mul_r [in CoqApprox.coeff_inst]
FullXR.mask0mul_l [in CoqApprox.coeff_inst]
FullXR.tadd_assoc [in CoqApprox.coeff_inst]
FullXR.tadd_comm [in CoqApprox.coeff_inst]
FullXR.tadd_zeror [in CoqApprox.coeff_inst]
FullXR.tadd_zerol [in CoqApprox.coeff_inst]
FullXR.tmul_distrr [in CoqApprox.coeff_inst]
FullXR.tmul_distrl [in CoqApprox.coeff_inst]
FullXR.tmul_assoc [in CoqApprox.coeff_inst]
FullXR.tmul_comm [in CoqApprox.coeff_inst]
FullXR.tmul_oner [in CoqApprox.coeff_inst]
FullXR.tmul_onel [in CoqApprox.coeff_inst]
FullXR.tpow_opp [in CoqApprox.coeff_inst]
FullXR.tpow_S [in CoqApprox.coeff_inst]
FullXR.tpow_0 [in CoqApprox.coeff_inst]


H

head_loopN [in CoqApprox.basic_rec]
head_rec2down [in CoqApprox.basic_rec]
head_loop2 [in CoqApprox.basic_rec]
head_rec1down [in CoqApprox.basic_rec]
head_loop1 [in CoqApprox.basic_rec]
head_cons [in CoqApprox.seq_compl]


I

inhR [in CoqApprox.Rstruct]
intro_unit_R [in CoqApprox.Rstruct]


L

lastN_Ttoseq [in CoqApprox.nary_tuple]
last_rev [in CoqApprox.seq_compl]
left_distr_Xmul_Xadd [in CoqApprox.xreal_ssr_compat]
LinkSeqPolyMonomUp.link_tnth_set_nth_nil [in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.link_tsize_set_nth_nil [in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.link_tmul_tail [in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.link_tmul_trunc [in CoqApprox.poly_inst_seq]
loopNE [in CoqApprox.basic_rec]
loopNS_ex [in CoqApprox.basic_rec]
loop1E [in CoqApprox.basic_rec]
loop1SE [in CoqApprox.basic_rec]
loop1S_ex [in CoqApprox.basic_rec]
loop2E [in CoqApprox.basic_rec]
loop2S_ex [in CoqApprox.basic_rec]
ltn_subr [in CoqApprox.seq_compl]


M

map_Tnth_enum [in CoqApprox.nary_tuple]
minnl [in CoqApprox.seq_compl]
minnr [in CoqApprox.seq_compl]


N

nat_ind_gen [in CoqApprox.seq_compl]
not_Xnan_Xreal_fun [in CoqApprox.xreal_ssr_compat]
nth_recNup_indep [in CoqApprox.basic_rec]
nth_recNdown_indep [in CoqApprox.basic_rec]
nth_recNdown_dflt2 [in CoqApprox.basic_rec]
nth_recNdown [in CoqApprox.basic_rec]
nth_rec2up_indep [in CoqApprox.basic_rec]
nth_rec2down_indep [in CoqApprox.basic_rec]
nth_rec2down_dflt2 [in CoqApprox.basic_rec]
nth_rec2down [in CoqApprox.basic_rec]
nth_rec1down_dflt2 [in CoqApprox.basic_rec]
nth_rec1down [in CoqApprox.basic_rec]
nth_defaults [in CoqApprox.basic_rec]
nth_mkTuple [in CoqApprox.nary_tuple]
nth_mkTupleO [in CoqApprox.nary_tuple]
nth_Xderive_pt_var [in CoqApprox.derive_compl]
nth_Xderive_pt_cst [in CoqApprox.derive_compl]
nth_Xderive_pt_cos [in CoqApprox.derive_compl]
nth_derivable_pt_cos [in CoqApprox.derive_compl]
nth_Xderive_pt_sin [in CoqApprox.derive_compl]
nth_derivable_pt_sin [in CoqApprox.derive_compl]
nth_Xderive_pt_invsqrt [in CoqApprox.derive_compl]
nth_Xderive_pt_sqrt [in CoqApprox.derive_compl]
nth_derivable_pt_sqrt [in CoqApprox.derive_compl]
nth_derivable_pt_power [in CoqApprox.derive_compl]
nth_Xderive_pt_inv [in CoqApprox.derive_compl]
nth_derivable_pt_inv [in CoqApprox.derive_compl]
nth_derivable_pt_inv_pow [in CoqApprox.derive_compl]
nth_Xderive_pt_pow [in CoqApprox.derive_compl]
nth_derivable_pt_pow [in CoqApprox.derive_compl]
nth_Xderive_pt_exp [in CoqApprox.derive_compl]
nth_derivable_pt_exp [in CoqApprox.derive_compl]
nth_map2 [in CoqApprox.seq_compl]
nth1 [in CoqApprox.seq_compl]
nuncurry_ncurry [in CoqApprox.basic_rec]
nuncurry_const [in CoqApprox.basic_rec]


O

ordinal1 [in CoqApprox.xreal_ssr_compat]


P

pickR_ext [in CoqApprox.Rstruct]
pickR_ex [in CoqApprox.Rstruct]
pickR_some [in CoqApprox.Rstruct]
PolyMap.tnth_polymap [in CoqApprox.taylor_model_float_sharp]
PolyMap.tsize_polymap [in CoqApprox.taylor_model_float_sharp]
predn_leq [in CoqApprox.seq_compl]


R

real_fieldMixin [in CoqApprox.Rstruct]
real_idomainMixin [in CoqApprox.Rstruct]
recNdownE [in CoqApprox.basic_rec]
recNdown_correct [in CoqApprox.basic_rec]
recNdown_init_correct [in CoqApprox.basic_rec]
recNup_correct [in CoqApprox.basic_rec]
recNup_init_correct [in CoqApprox.basic_rec]
rec1down_co0' [in CoqApprox.basic_rec]
rec1down_co0 [in CoqApprox.basic_rec]
rec1down_nth_indep [in CoqApprox.basic_rec]
rec1down_correct [in CoqApprox.basic_rec]
rec1up_co0' [in CoqApprox.basic_rec]
rec1up_co0 [in CoqApprox.basic_rec]
rec1up_nth_indep [in CoqApprox.basic_rec]
rec1up_correct [in CoqApprox.basic_rec]
rec1up_nth_last [in CoqApprox.basic_rec]
rec2down_co1 [in CoqApprox.basic_rec]
rec2down_co0 [in CoqApprox.basic_rec]
rec2down_correct' [in CoqApprox.basic_rec]
rec2down_correct [in CoqApprox.basic_rec]
rec2up_co1 [in CoqApprox.basic_rec]
rec2up_co0 [in CoqApprox.basic_rec]
rec2up_correct' [in CoqApprox.basic_rec]
rec2up_correct [in CoqApprox.basic_rec]
rec2up_nth_last [in CoqApprox.basic_rec]
Req_EM_T [in CoqApprox.Rstruct]
rev_iota [in CoqApprox.poly_inst_seq]
rev'E [in CoqApprox.basic_rec]
RgeP [in CoqApprox.Rstruct]
RgtP [in CoqApprox.Rstruct]
right_distr_Rmult_Rplus [in CoqApprox.xreal_ssr_compat]
RinvxRmult [in CoqApprox.Rstruct]
Rinvx_out [in CoqApprox.Rstruct]
RleP [in CoqApprox.Rstruct]
RltP [in CoqApprox.Rstruct]
rmlast_cons [in CoqApprox.seq_compl]
RmultA [in CoqApprox.Rstruct]
RmultRinvx [in CoqApprox.Rstruct]
Rneq_lt [in CoqApprox.xreal_ssr_compat]
Rolle_lim [in CoqApprox.taylor_thm]
RplusA [in CoqApprox.Rstruct]
R1_neq_0 [in CoqApprox.Rstruct]


S

SeqPolyMonomUp.mul_coeffE' [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.size_tsub [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.size_topp [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.teval_polyCons [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.teval_polyNil [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tfold_polyCons [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tfold_polyNil [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tlastN_spec [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_out [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_set_nth_neq [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_set_nth_eq [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_polyNil [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_polyCons [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_tadd [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth_map [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tpoly_ind [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trecN_spec [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trecN_spec0 [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec1_spec [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec1_spec0 [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec2_spec [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec2_spec1 [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec2_spec0 [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_set_nth [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_mul_tail [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_mul_trunc [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_polyNil [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_polyCons [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_trecN [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_trec2 [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_trec1 [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_tadd [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize_map [in CoqApprox.poly_inst_seq]
size_recNup [in CoqApprox.basic_rec]
size_recNdown [in CoqApprox.basic_rec]
size_loopN [in CoqApprox.basic_rec]
size_rec2up [in CoqApprox.basic_rec]
size_rec2down [in CoqApprox.basic_rec]
size_loop2 [in CoqApprox.basic_rec]
size_rec1up [in CoqApprox.basic_rec]
size_rec1down [in CoqApprox.basic_rec]
size_loop1 [in CoqApprox.basic_rec]
size_Tuple [in CoqApprox.nary_tuple]
size_map2 [in CoqApprox.seq_compl]
size_take_minn [in CoqApprox.seq_compl]
slideN_lastN [in CoqApprox.basic_rec]
subset_refl [in CoqApprox.interval_compl]
sum_f_to_big [in CoqApprox.xreal_ssr_compat]


T

takeN_Ttoseq [in CoqApprox.nary_tuple]
take_drop_rev [in CoqApprox.nary_tuple]
TaylorModelFloat.contains_bnd2 [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.Imask_mask [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_tm_correct [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_mid_nan [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_mid_correct [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.sub_midp_contains_0 [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.teval_contains_0 [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.Xsub_diag_eq [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.Xsub_Xnan_r [in CoqApprox.taylor_model_float_sharp]
TaylorModel.bigXadd_real [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd_XP [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd_Si [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd_ni [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd_nS [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd'_real [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd'_XP [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd'_real_S [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bigXadd'_XP_S [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_contains_upper [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_contains_lower [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_upper_Xnan [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_lower_Xnan [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_Iupper [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_Ilower [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_IIbnd [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_IInan [in CoqApprox.taylor_model_int_sharp]
TaylorModel.bounded_singleton_contains_lower_upper [in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_IIbnd [in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_Xgt [in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_lower_or_upper [in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_lower_or_upper_Xreal [in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_IIbnd_Xreal [in CoqApprox.taylor_model_int_sharp]
TaylorModel.contains_lower_le_upper [in CoqApprox.taylor_model_int_sharp]
TaylorModel.convert_teval [in CoqApprox.taylor_model_int_sharp]
TaylorModel.derivable_pt_lim_pow_sub [in CoqApprox.taylor_model_int_sharp]
TaylorModel.eq_Xcst_sign [in CoqApprox.taylor_model_int_sharp]
TaylorModel.eq'_Xcst_sign [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iadd_Isub_aux [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iadd_zero_subset_r [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iadd_zero_subset_l [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iadd_Inan_propagate_r [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iadd_Inan_propagate_l [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ilower_Xreal [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ilower_bnd [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Imul_Inan_propagate_r [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Imul_Inan_propagate_l [in CoqApprox.taylor_model_int_sharp]
TaylorModel.in_poly_bound [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ipow_Inan_propagate [in CoqApprox.taylor_model_int_sharp]
TaylorModel.isNNegOrNPos_false [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Isub_Inan_propagate_r [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Isub_Inan_propagate_l [in CoqApprox.taylor_model_int_sharp]
TaylorModel.is_horner_mask [in CoqApprox.taylor_model_int_sharp]
TaylorModel.is_horner_pos [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iupper_Xreal [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Iupper_bnd [in CoqApprox.taylor_model_int_sharp]
TaylorModel.i_validTM_Ztech [in CoqApprox.taylor_model_int_sharp]
TaylorModel.i_validTM_TLrem [in CoqApprox.taylor_model_int_sharp]
TaylorModel.i_validTM_subset_X0 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.le_lower_or [in CoqApprox.taylor_model_int_sharp]
TaylorModel.le_upper_or [in CoqApprox.taylor_model_int_sharp]
TaylorModel.lower_odd_Xneg_over [in CoqApprox.taylor_model_int_sharp]
TaylorModel.lower_odd_Xpos_over [in CoqApprox.taylor_model_int_sharp]
TaylorModel.lower_even_Xneg_over [in CoqApprox.taylor_model_int_sharp]
TaylorModel.lower_even_Xpos_over [in CoqApprox.taylor_model_int_sharp]
TaylorModel.lower_le [in CoqApprox.taylor_model_int_sharp]
TaylorModel.mul_0_contains_0_r [in CoqApprox.taylor_model_int_sharp]
TaylorModel.mul_0_contains_0_l [in CoqApprox.taylor_model_int_sharp]
TaylorModel.notIInan_IIbnd [in CoqApprox.taylor_model_int_sharp]
TaylorModel.not_and_impl [in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_eval_tm_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_eval_tm_correct_aux [in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_eval_tm_correct_gen [in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_eval_tm_correct_aux_gen [in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_mul [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Poly_size' [in CoqApprox.taylor_model_int_sharp]
TaylorModel.powerRZ_1_even [in CoqApprox.taylor_model_int_sharp]
TaylorModel.powerRZ_pow [in CoqApprox.taylor_model_int_sharp]
TaylorModel.pow_Rabs_sign [in CoqApprox.taylor_model_int_sharp]
TaylorModel.pow_contains_0 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.proj_fun_id [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_1_r [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_twice [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_neg_compat_rev [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_neg_compat [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_pos_compat_rev [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rdiv_pos_compat [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rlt_neq_sym [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Rlt_neq [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ropp_le_0 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.size_poly_eval_tm [in CoqApprox.taylor_model_int_sharp]
TaylorModel.size_TM_mul [in CoqApprox.taylor_model_int_sharp]
TaylorModel.size_TM_add [in CoqApprox.taylor_model_int_sharp]
TaylorModel.subset_real_contains [in CoqApprox.taylor_model_int_sharp]
TaylorModel.subset_sub_contains_0 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.teval_poly_nan [in CoqApprox.taylor_model_int_sharp]
TaylorModel.teval_in_nan [in CoqApprox.taylor_model_int_sharp]
TaylorModel.teval_contains [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TMset0_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_div_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_inv_comp_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_comp_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_fun_eq [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_mul_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_mul_correct_gen [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_add_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_add_correct_gen [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_cos_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_sin_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_invsqrt_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_sqrt_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_exp_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_inv_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_var_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_cst_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_rec2_correct' [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_rec2_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_rec1_correct' [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_rec1_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.tpolyNil_size0 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.upper_Xneg_over [in CoqApprox.taylor_model_int_sharp]
TaylorModel.upper_Xpos_over [in CoqApprox.taylor_model_int_sharp]
TaylorModel.upper_le [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xcmp_lt_imp_fun [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xcmp_gt_imp_fun [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xcmp_same [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta_real [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta_idem' [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta_idem [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta'_real [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xder [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_delta [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_pt_sub_r [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_pt_sub' [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_cst_sign [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_neg_imp_decr [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_pos_imp_incr [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_over_propagate' [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_over_propagate [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdiv_1_r [in CoqApprox.taylor_model_int_sharp]
TaylorModel.XDn_Xnan' [in CoqApprox.taylor_model_int_sharp]
TaylorModel.XDn_Xnan [in CoqApprox.taylor_model_int_sharp]
TaylorModel.XDn_0 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xeq_imp [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xmonot_contains_weak [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xmonot_contains [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xnan_ex_S [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xnan_ex_not [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xnan_ex_or [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xneg_Xadd [in CoqApprox.taylor_model_int_sharp]
TaylorModel.XPoly_nth0 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xreal_over_imp [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xsub_0_r [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xund_contra [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xund_imp [in CoqApprox.taylor_model_int_sharp]
TaylorModel.ZEven_pow_le [in CoqApprox.taylor_model_int_sharp]
TaylorModel.ZOdd_pow_le [in CoqApprox.taylor_model_int_sharp]
TaylorModel.ZtechE1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.ZtechE2 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ztech_derive_sign [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Zumkeller_monot_rem [in CoqApprox.taylor_model_int_sharp]
Taylor_Lagrange [in CoqApprox.taylor_thm]
TcastE [in CoqApprox.nary_tuple]
TcastK [in CoqApprox.nary_tuple]
TcastKV [in CoqApprox.nary_tuple]
Tcast_trans [in CoqApprox.nary_tuple]
Tcast_id [in CoqApprox.nary_tuple]
TheadE [in CoqApprox.nary_tuple]
Tnth_lastN [in CoqApprox.nary_tuple]
Tnth_mkTuple [in CoqApprox.nary_tuple]
Tnth_mkTupleO [in CoqApprox.nary_tuple]
Tnth_ord_Tuple [in CoqApprox.nary_tuple]
Tnth_Tuplify [in CoqApprox.nary_tuple]
tnth_tuplify [in CoqApprox.nary_tuple]
Tnth_map_Tuple [in CoqApprox.nary_tuple]
Tnth_nth [in CoqApprox.nary_tuple]
Tnth_default [in CoqApprox.nary_tuple]
Tnth0 [in CoqApprox.nary_tuple]
TofseqK [in CoqApprox.nary_tuple]
TtoseqK [in CoqApprox.nary_tuple]
Ttoseq_slideN [in CoqApprox.basic_rec]
Ttoseq_slideN_aux [in CoqApprox.basic_rec]
Ttoseq_lastN_rev' [in CoqApprox.nary_tuple]
Ttoseq_lastN_drop' [in CoqApprox.nary_tuple]
Ttoseq_lastN_rev [in CoqApprox.nary_tuple]
Ttoseq_lastN_drop [in CoqApprox.nary_tuple]
Ttoseq_takeN' [in CoqApprox.nary_tuple]
Ttoseq_takeN [in CoqApprox.nary_tuple]
Ttoseq_ord_Tuple [in CoqApprox.nary_tuple]
Ttoseq_Tuplify [in CoqApprox.nary_tuple]
Ttoseq_iota [in CoqApprox.nary_tuple]
Ttoseq_nseq [in CoqApprox.nary_tuple]
Ttoseq_map [in CoqApprox.nary_tuple]
Ttoseq_inj [in CoqApprox.nary_tuple]
Tuple_map_ord [in CoqApprox.nary_tuple]
Tuple0 [in CoqApprox.nary_tuple]
Tuple0eq [in CoqApprox.nary_tuple]
TuplifyK [in CoqApprox.nary_tuple]
tuplifyK [in CoqApprox.nary_tuple]


V

val_tuplify [in CoqApprox.nary_tuple]


X

XaddA [in CoqApprox.xreal_ssr_compat]
XaddC [in CoqApprox.xreal_ssr_compat]
Xadd0 [in CoqApprox.xreal_ssr_compat]
Xderive_propagate' [in CoqApprox.xreal_ssr_compat]
Xderive_propagate [in CoqApprox.xreal_ssr_compat]
Xderive_pt_mulXmask [in CoqApprox.xreal_ssr_compat]
Xderive_pt_Xpow [in CoqApprox.xreal_ssr_compat]
Xderive_pt_mul_const [in CoqApprox.derive_compl]
XD_Xreal [in CoqApprox.xreal_ssr_compat]
XD_Xnan_propagate [in CoqApprox.xreal_ssr_compat]
Xinv_1 [in CoqApprox.xreal_ssr_compat]
XmulA [in CoqApprox.xreal_ssr_compat]
XmulC [in CoqApprox.xreal_ssr_compat]
Xmul_Xreal [in CoqApprox.xreal_ssr_compat]
Xmul0 [in CoqApprox.xreal_ssr_compat]
Xneg_as_Xmul [in CoqApprox.interval_compl]
Xpow_Xnan [in CoqApprox.xreal_ssr_compat]
Xpow_Xreal [in CoqApprox.xreal_ssr_compat]
Xpow_idem [in CoqApprox.xreal_ssr_compat]
Xreal_irrelevance [in CoqApprox.xreal_ssr_compat]
XReq_EM_T [in CoqApprox.xreal_ssr_compat]
Xsub_Xnan_r [in CoqApprox.xreal_ssr_compat]
Xsub_Xreal_r [in CoqApprox.xreal_ssr_compat]
Xsub_Xreal_l [in CoqApprox.xreal_ssr_compat]
Xsub_Xadd_distr [in CoqApprox.xreal_ssr_compat]
XTaylor_Lagrange [in CoqApprox.xreal_ssr_compat]
X0add [in CoqApprox.xreal_ssr_compat]
X0mul [in CoqApprox.xreal_ssr_compat]


Z

zeroF [in CoqApprox.xreal_ssr_compat]
zeroT [in CoqApprox.xreal_ssr_compat]



Section Index

C

cst_var [in CoqApprox.derive_compl]


D

DefixN [in CoqApprox.basic_rec]
Defix1 [in CoqApprox.basic_rec]
Defix2 [in CoqApprox.basic_rec]


F

Fold [in CoqApprox.seq_compl]


G

generic [in CoqApprox.derive_compl]


H

Head_Last [in CoqApprox.seq_compl]


I

inverse [in CoqApprox.derive_compl]


M

Map2 [in CoqApprox.seq_compl]


N

NaryTuple [in CoqApprox.nary_tuple]
NaryTupleCast [in CoqApprox.nary_tuple]
NaryTupleMap [in CoqApprox.nary_tuple]
NaryTupleMk [in CoqApprox.nary_tuple]
NaryTupleMkNat [in CoqApprox.nary_tuple]
NaryTupleSeq [in CoqApprox.nary_tuple]
NaryTuple1 [in CoqApprox.nary_tuple]
NatCompl [in CoqApprox.seq_compl]
NDerive [in CoqApprox.xreal_ssr_compat]
nth_pow [in CoqApprox.derive_compl]
nth_exp [in CoqApprox.derive_compl]


P

power [in CoqApprox.derive_compl]
ProofN [in CoqApprox.basic_rec]
ProofN' [in CoqApprox.basic_rec]


S

SeqPolyMonomUp.PrecIsPropagated [in CoqApprox.poly_inst_seq]
sin_cos [in CoqApprox.derive_compl]
square_root [in CoqApprox.derive_compl]


T

Take [in CoqApprox.seq_compl]
takeN_lastN [in CoqApprox.nary_tuple]
TaylorLagrange [in CoqApprox.taylor_thm]
TaylorLagrange.CorTL [in CoqApprox.taylor_thm]
TaylorLagrange.TL [in CoqApprox.taylor_thm]
TaylorModel.PrecArgument [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.Corollaries [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.GenericProof [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec1_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TaylorModel [in CoqApprox.taylor_model_int_sharp]
TaylorPoly.PrecIsPropagated [in CoqApprox.taylor_poly]
TaylorRec.PrecIsPropagated [in CoqApprox.taylor_poly]
TestN [in CoqApprox.basic_rec]
Test1 [in CoqApprox.basic_rec]
Test2 [in CoqApprox.basic_rec]
Tuplify [in CoqApprox.nary_tuple]



Notation Index

B

--> _ [in CoqApprox.coeff_inst]


F

--> _ [in CoqApprox.coeff_inst]
--> _ [in CoqApprox.coeff_inst]


S

_ * _ [in CoqApprox.poly_inst_seq]
_ + _ [in CoqApprox.poly_inst_seq]


T

_ - _ [in CoqApprox.taylor_model_int_sharp]
_ + _ [in CoqApprox.taylor_model_int_sharp]
_ / _ [in CoqApprox.taylor_poly]
_ * _ [in CoqApprox.taylor_poly]
_ - _ [in CoqApprox.taylor_poly]
_ + _ [in CoqApprox.taylor_poly]


other

[ Tuple _ | 0 <= _ < _ ] (form_scope) [in CoqApprox.nary_tuple]
[ Tuple _ | _ < _ ] (form_scope) [in CoqApprox.nary_tuple]
[ Tuple _ ; .. ; _ ] (form_scope) [in CoqApprox.nary_tuple]
[ Tuple _ ] (form_scope) [in CoqApprox.nary_tuple]
[ Tuple ] (form_scope) [in CoqApprox.nary_tuple]
[ Tnth _ _ ] (form_scope) [in CoqApprox.nary_tuple]
[ Tuple of _ ] (form_scope) [in CoqApprox.nary_tuple]
_ ^ _ (XR_scope) [in CoqApprox.xreal_ssr_compat]
_ / _ (XR_scope) [in CoqApprox.xreal_ssr_compat]
_ * _ (XR_scope) [in CoqApprox.xreal_ssr_compat]
- _ (XR_scope) [in CoqApprox.xreal_ssr_compat]
_ - _ (XR_scope) [in CoqApprox.xreal_ssr_compat]
_ + _ (XR_scope) [in CoqApprox.xreal_ssr_compat]
_ *2^ _ [in CoqApprox.test_exp_sin]



Constructor Index

R

RigPolyApprox.RPA [in CoqApprox.poly_datatypes]


T

TaylorModel.Compat_rec2 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Compat_rec1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Extension2N [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Extension3N [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Nth_Xderive [in CoqApprox.taylor_model_int_sharp]
TaylorModel.ValidPoly [in CoqApprox.taylor_model_int_sharp]
TaylorModel.ValidXPoly [in CoqApprox.taylor_model_int_sharp]



Inductive Index

T

TaylorModel.compat_rec2 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.compat_rec1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.extension2N [in CoqApprox.taylor_model_int_sharp]
TaylorModel.extension3N [in CoqApprox.taylor_model_int_sharp]
TaylorModel.nth_Xderive [in CoqApprox.taylor_model_int_sharp]



Abbreviation Index

C

Cab [in CoqApprox.taylor_thm]


E

ExactSeqPolyMonomUp.Ctpow [in CoqApprox.poly_inst_seq]


I

IIbnd [in CoqApprox.interval_compl]
IInan [in CoqApprox.interval_compl]


O

Oab [in CoqApprox.taylor_thm]


S

SliceExactMonomPolyOps.Ctpow [in CoqApprox.poly_datatypes]
SliceExactPowDivOps.tpow [in CoqApprox.poly_datatypes]
subset_ [in CoqApprox.interval_compl]


T

TaylorModelFloat.f_approx [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_error [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_RPA [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_rpa [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_poly [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f_type [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f2x [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_poly_map [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_eval [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_prec [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_approx [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_error [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_RPA [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_rpa [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_poly [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i_type [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2ix [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.subset_ [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.x_eval [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.x_poly [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.x_type [in CoqApprox.taylor_model_float_sharp]
TaylorModel.Ibnd2 [in CoqApprox.taylor_model_int_sharp]
Tcoeff [in CoqApprox.taylor_thm]
Tsum [in CoqApprox.taylor_thm]
Tterm [in CoqApprox.taylor_thm]



Definition Index

B

BaseZ.T [in CoqApprox.coeff_inst]
BaseZ.tadd [in CoqApprox.coeff_inst]
BaseZ.tmul [in CoqApprox.coeff_inst]
BaseZ.tone [in CoqApprox.coeff_inst]
BaseZ.topp [in CoqApprox.coeff_inst]
BaseZ.tsub [in CoqApprox.coeff_inst]
BaseZ.tzero [in CoqApprox.coeff_inst]
BaseZ.U [in CoqApprox.coeff_inst]


C

catrev' [in CoqApprox.basic_rec]
cons_Tuple [in CoqApprox.nary_tuple]


E

eqr [in CoqApprox.Rstruct]
eqX [in CoqApprox.xreal_ssr_compat]
ExactSeqPolyMonomUp.Cadd_addlaw [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.Cadd_comm [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.Cadd_monoid [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.Cmul_comm [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.Cmul_monoid [in CoqApprox.poly_inst_seq]


F

factz [in CoqApprox.basic_rec]
fibz [in CoqApprox.basic_rec]
FullInt.T [in CoqApprox.coeff_inst]
FullInt.tadd [in CoqApprox.coeff_inst]
FullInt.tcos [in CoqApprox.coeff_inst]
FullInt.tcst [in CoqApprox.coeff_inst]
FullInt.tdiv [in CoqApprox.coeff_inst]
FullInt.texp [in CoqApprox.coeff_inst]
FullInt.tinv [in CoqApprox.coeff_inst]
FullInt.tinvsqrt [in CoqApprox.coeff_inst]
FullInt.tmul [in CoqApprox.coeff_inst]
FullInt.tnat [in CoqApprox.coeff_inst]
FullInt.tone [in CoqApprox.coeff_inst]
FullInt.topp [in CoqApprox.coeff_inst]
FullInt.tpower_int [in CoqApprox.coeff_inst]
FullInt.tsin [in CoqApprox.coeff_inst]
FullInt.tsqr [in CoqApprox.coeff_inst]
FullInt.tsqrt [in CoqApprox.coeff_inst]
FullInt.tsub [in CoqApprox.coeff_inst]
FullInt.tzero [in CoqApprox.coeff_inst]
FullInt.U [in CoqApprox.coeff_inst]
FullReal.T [in CoqApprox.coeff_inst]
FullReal.tadd [in CoqApprox.coeff_inst]
FullReal.tcos [in CoqApprox.coeff_inst]
FullReal.tcst [in CoqApprox.coeff_inst]
FullReal.tdiv [in CoqApprox.coeff_inst]
FullReal.texp [in CoqApprox.coeff_inst]
FullReal.tinv [in CoqApprox.coeff_inst]
FullReal.tinvsqrt [in CoqApprox.coeff_inst]
FullReal.tmul [in CoqApprox.coeff_inst]
FullReal.tnat [in CoqApprox.coeff_inst]
FullReal.tone [in CoqApprox.coeff_inst]
FullReal.topp [in CoqApprox.coeff_inst]
FullReal.tpower_int [in CoqApprox.coeff_inst]
FullReal.tsin [in CoqApprox.coeff_inst]
FullReal.tsqr [in CoqApprox.coeff_inst]
FullReal.tsqrt [in CoqApprox.coeff_inst]
FullReal.tsub [in CoqApprox.coeff_inst]
FullReal.tzero [in CoqApprox.coeff_inst]
FullReal.U [in CoqApprox.coeff_inst]
FullXR.T [in CoqApprox.coeff_inst]
FullXR.tadd [in CoqApprox.coeff_inst]
FullXR.tcos [in CoqApprox.coeff_inst]
FullXR.tcst [in CoqApprox.coeff_inst]
FullXR.tdiv [in CoqApprox.coeff_inst]
FullXR.texp [in CoqApprox.coeff_inst]
FullXR.tinv [in CoqApprox.coeff_inst]
FullXR.tinvsqrt [in CoqApprox.coeff_inst]
FullXR.tmul [in CoqApprox.coeff_inst]
FullXR.tnat [in CoqApprox.coeff_inst]
FullXR.tone [in CoqApprox.coeff_inst]
FullXR.topp [in CoqApprox.coeff_inst]
FullXR.tpow [in CoqApprox.coeff_inst]
FullXR.tpower_int [in CoqApprox.coeff_inst]
FullXR.tsin [in CoqApprox.coeff_inst]
FullXR.tsqr [in CoqApprox.coeff_inst]
FullXR.tsqrt [in CoqApprox.coeff_inst]
FullXR.tsub [in CoqApprox.coeff_inst]
FullXR.tzero [in CoqApprox.coeff_inst]
FullXR.U [in CoqApprox.coeff_inst]


H

hb [in CoqApprox.seq_compl]
hide_let [in CoqApprox.basic_rec]


I

iota_Tuple [in CoqApprox.nary_tuple]
Irnd [in CoqApprox.test_exp_sin]


L

lastN [in CoqApprox.nary_tuple]
LinkIntX.contains_pointwise [in CoqApprox.rpa_inst]
LinkIntX.contains_pointwise_until [in CoqApprox.rpa_inst]
LinkSeqPolyMonomUp.contains_pointwise [in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.contains_pointwise_until [in CoqApprox.poly_inst_seq]
loopN [in CoqApprox.basic_rec]
loop1 [in CoqApprox.basic_rec]
loop2 [in CoqApprox.basic_rec]


M

map_Tuple [in CoqApprox.nary_tuple]
map2 [in CoqApprox.seq_compl]
MaskBaseF_NE.tcst [in CoqApprox.coeff_inst]
MaskBaseF_NE.tsub [in CoqApprox.coeff_inst]
MaskBaseF_NE.topp [in CoqApprox.coeff_inst]
MaskBaseF_NE.tmul [in CoqApprox.coeff_inst]
MaskBaseF_NE.tadd [in CoqApprox.coeff_inst]
MaskBaseF_NE.tone [in CoqApprox.coeff_inst]
MaskBaseF_NE.tzero [in CoqApprox.coeff_inst]
MaskBaseF_NE.T [in CoqApprox.coeff_inst]
MaskBaseF_NE.U [in CoqApprox.coeff_inst]
MaskBaseF.T [in CoqApprox.coeff_inst]
MaskBaseF.tadd [in CoqApprox.coeff_inst]
MaskBaseF.tcst [in CoqApprox.coeff_inst]
MaskBaseF.tmul [in CoqApprox.coeff_inst]
MaskBaseF.tone [in CoqApprox.coeff_inst]
MaskBaseF.topp [in CoqApprox.coeff_inst]
MaskBaseF.tsub [in CoqApprox.coeff_inst]
MaskBaseF.tzero [in CoqApprox.coeff_inst]
MaskBaseF.U [in CoqApprox.coeff_inst]
mkTuple [in CoqApprox.nary_tuple]
mkTupleO [in CoqApprox.nary_tuple]


N

nseq_Tuple [in CoqApprox.nary_tuple]
nth_Xcos [in CoqApprox.derive_compl]
nth_Xsin [in CoqApprox.derive_compl]
nth_Xderive_pt [in CoqApprox.derive_compl]
nth_derivable_pt [in CoqApprox.derive_compl]
nuncurry2 [in CoqApprox.coeff_inst]


O

ord_Tuple [in CoqApprox.nary_tuple]


P

pickR [in CoqApprox.Rstruct]
PolyMap.tpolymap [in CoqApprox.taylor_model_float_sharp]
PolyMap.tpolymap_polyNil [in CoqApprox.taylor_model_float_sharp]
PolyMap.tpolymap_polyCons [in CoqApprox.taylor_model_float_sharp]


R

Radd_add_law [in CoqApprox.Rstruct]
Radd_comoid [in CoqApprox.Rstruct]
Radd_monoid [in CoqApprox.Rstruct]
real_field [in CoqApprox.Rstruct]
real_fieldIdomainMixin [in CoqApprox.Rstruct]
real_idomainType [in CoqApprox.Rstruct]
real_comUnitRingType [in CoqApprox.Rstruct]
real_unitRing [in CoqApprox.Rstruct]
real_unitRingMixin [in CoqApprox.Rstruct]
real_comringType [in CoqApprox.Rstruct]
real_ringType [in CoqApprox.Rstruct]
real_ringMixin [in CoqApprox.Rstruct]
real_zmodType [in CoqApprox.Rstruct]
real_zmodMixin [in CoqApprox.Rstruct]
real_eqType [in CoqApprox.Rstruct]
real_eqMixin [in CoqApprox.Rstruct]
recNdown [in CoqApprox.basic_rec]
recNup [in CoqApprox.basic_rec]
rec1down [in CoqApprox.basic_rec]
rec1up [in CoqApprox.basic_rec]
rec2down [in CoqApprox.basic_rec]
rec2up [in CoqApprox.basic_rec]
rev' [in CoqApprox.basic_rec]
Rgeb [in CoqApprox.Rstruct]
Rgtb [in CoqApprox.Rstruct]
Rinvx [in CoqApprox.Rstruct]
Rleb [in CoqApprox.Rstruct]
Rltb [in CoqApprox.Rstruct]
rmlast [in CoqApprox.seq_compl]
Rmul_mul_law [in CoqApprox.Rstruct]
Rmul_comoid [in CoqApprox.Rstruct]
Rmul_monoid [in CoqApprox.Rstruct]
R_choiceType [in CoqApprox.Rstruct]
R_choiceMixin [in CoqApprox.Rstruct]


S

SeqPolyMonomUp.mul_coeff [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.T [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tadd [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.teval [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tfold [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tlastN [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tmap [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tmul [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tmul_tail [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tmul_trunc [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tnth [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tone [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.topp [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tpolyCons [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tpolyNil [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trecN [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec1 [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.trec2 [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tset_nth [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsize [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tsub [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.tzero [in CoqApprox.poly_inst_seq]
SeqPolyMonomUp.U [in CoqApprox.poly_inst_seq]
slideN [in CoqApprox.basic_rec]
slideN_aux [in CoqApprox.basic_rec]
snd' [in CoqApprox.basic_rec]


T

takeN [in CoqApprox.nary_tuple]
TaylorModelFloat.f_validTM [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f2i [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.f2x_poly [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_tm [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_rem [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_poly [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.i2f_mid [in CoqApprox.taylor_model_float_sharp]
TaylorModel.IP_rec2 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.IP_rec1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.isNNegOrNPos [in CoqApprox.taylor_model_int_sharp]
TaylorModel.i_validTM [in CoqApprox.taylor_model_int_sharp]
TaylorModel.mul_error [in CoqApprox.taylor_model_int_sharp]
TaylorModel.poly_eval_tm [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TLrem [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TMset0 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_div [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_inv_comp [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_comp [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_type [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_mul [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_add [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_cos [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_sin [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_invsqrt [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_sqrt [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_exp [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_inv [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_var [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TM_cst [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xcst_sign [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdecr [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta_mask [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta_big [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xdelta'_big [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xderive_over [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xincr [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xmonot [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xnan_ex [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xneg_over [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xpos_over [in CoqApprox.taylor_model_int_sharp]
TaylorModel.XP_rec2 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.XP_rec1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xreal_over' [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Xreal_over [in CoqApprox.taylor_model_int_sharp]
TaylorModel.Ztech [in CoqApprox.taylor_model_int_sharp]
TaylorPoly.T_invsqrt [in CoqApprox.taylor_poly]
TaylorPoly.T_sqrt [in CoqApprox.taylor_poly]
TaylorPoly.T_cos [in CoqApprox.taylor_poly]
TaylorPoly.T_sin [in CoqApprox.taylor_poly]
TaylorPoly.T_exp [in CoqApprox.taylor_poly]
TaylorPoly.T_inv [in CoqApprox.taylor_poly]
TaylorPoly.T_var [in CoqApprox.taylor_poly]
TaylorPoly.T_cst [in CoqApprox.taylor_poly]
TaylorRec.cos_rec [in CoqApprox.taylor_poly]
TaylorRec.cst_rec [in CoqApprox.taylor_poly]
TaylorRec.exp_rec [in CoqApprox.taylor_poly]
TaylorRec.invsqrt_rec [in CoqApprox.taylor_poly]
TaylorRec.inv_rec [in CoqApprox.taylor_poly]
TaylorRec.sin_rec [in CoqApprox.taylor_poly]
TaylorRec.sqrt_rec [in CoqApprox.taylor_poly]
TaylorRec.var_rec [in CoqApprox.taylor_poly]
Tcast [in CoqApprox.nary_tuple]
Thead [in CoqApprox.nary_tuple]
TM_comp_0.tm' [in CoqApprox.test_exp_sin]
TM_comp_0.tm [in CoqApprox.test_exp_sin]
TM_comp_0.tm_sin [in CoqApprox.test_exp_sin]
TM_comp_0.pr [in CoqApprox.test_exp_sin]
TM_comp_0.deg [in CoqApprox.test_exp_sin]
TM_comp_0.X0 [in CoqApprox.test_exp_sin]
TM_comp_0.c [in CoqApprox.test_exp_sin]
TM_comp_0.X [in CoqApprox.test_exp_sin]
TM_comp_0.b [in CoqApprox.test_exp_sin]
TM_comp_0.a [in CoqApprox.test_exp_sin]
Tnth [in CoqApprox.nary_tuple]
Tofseq [in CoqApprox.nary_tuple]
Tsize [in CoqApprox.nary_tuple]
Ttoseq [in CoqApprox.nary_tuple]
Tuplify [in CoqApprox.nary_tuple]
tuplify [in CoqApprox.nary_tuple]


U

unit_R [in CoqApprox.Rstruct]


X

Xadd_comoid [in CoqApprox.xreal_ssr_compat]
Xadd_monoid [in CoqApprox.xreal_ssr_compat]
Xmul_comoid [in CoqApprox.xreal_ssr_compat]
Xmul_monoid [in CoqApprox.xreal_ssr_compat]
Xpow [in CoqApprox.xreal_ssr_compat]
Xpow_iter [in CoqApprox.xreal_ssr_compat]
Xreal_eqType [in CoqApprox.xreal_ssr_compat]
Xreal_eqMixin [in CoqApprox.xreal_ssr_compat]



Module Index

B

BaseOps [in CoqApprox.poly_datatypes]
BaseOps0 [in CoqApprox.poly_datatypes]
BaseZ [in CoqApprox.coeff_inst]


C

C [in CoqApprox.test_exp_sin]


E

ExactFullOps [in CoqApprox.poly_datatypes]
ExactMonomPolyOps [in CoqApprox.poly_datatypes]
ExactSeqPolyMonomUp [in CoqApprox.poly_inst_seq]
ExactSeqPolyMonomUp.M [in CoqApprox.poly_inst_seq]


F

F [in CoqApprox.test_exp_sin]
FloatIntervalOps [in CoqApprox.taylor_model_float_sharp]
FloatMonomPolyOps [in CoqApprox.rpa_inst]
FloatMonomPolyOps.Fl [in CoqApprox.rpa_inst]
FloatPolyOps [in CoqApprox.rpa_inst]
FloatPolyOps.Fl [in CoqApprox.rpa_inst]
FullInt [in CoqApprox.coeff_inst]
FullOps [in CoqApprox.poly_datatypes]
FullOps0 [in CoqApprox.poly_datatypes]
FullReal [in CoqApprox.coeff_inst]
FullXR [in CoqApprox.coeff_inst]


I

I [in CoqApprox.test_exp_sin]
IntMonomPolyOps [in CoqApprox.rpa_inst]
IntMonomPolyOps.Int [in CoqApprox.rpa_inst]
IntPolyOps [in CoqApprox.rpa_inst]
IntPolyOps.Int [in CoqApprox.rpa_inst]


L

Link [in CoqApprox.test_exp_sin]
LinkIntX [in CoqApprox.rpa_inst]
LinkIntXPr [in CoqApprox.poly_inst_seq]
LinkIntXPr.Pol [in CoqApprox.poly_inst_seq]
LinkIntXPr.PolX [in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp [in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.Pol [in CoqApprox.poly_inst_seq]
LinkSeqPolyMonomUp.PolX [in CoqApprox.poly_inst_seq]


M

MaskBaseF [in CoqApprox.coeff_inst]
MaskBaseF_NE [in CoqApprox.coeff_inst]
MaskBaseOps [in CoqApprox.poly_datatypes]
MaskBaseOps0 [in CoqApprox.poly_datatypes]
MonomPolyOps [in CoqApprox.poly_datatypes]


P

PolF [in CoqApprox.test_exp_sin]
PolI [in CoqApprox.test_exp_sin]
PolX [in CoqApprox.test_exp_sin]
PolyMap [in CoqApprox.taylor_model_float_sharp]
PolyOps [in CoqApprox.poly_datatypes]
PowDivOps [in CoqApprox.poly_datatypes]
PowDivOps0 [in CoqApprox.poly_datatypes]


R

RigPolyApprox [in CoqApprox.poly_datatypes]
RigPolyApproxFloat [in CoqApprox.taylor_model_float_sharp]
RigPolyApproxFloat.Fl [in CoqApprox.taylor_model_float_sharp]
RigPolyApproxInt [in CoqApprox.rpa_inst]


S

SeqPolyMonomUp [in CoqApprox.poly_inst_seq]
SeqPolyMonomUpFloat [in CoqApprox.poly_inst_seq]
SeqPolyMonomUpFloat.Fl [in CoqApprox.poly_inst_seq]
SeqPolyMonomUpInt [in CoqApprox.poly_inst_seq]
SeqPolyMonomUpInt.Int [in CoqApprox.poly_inst_seq]
SliceExactBaseOps [in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps [in CoqApprox.poly_datatypes]
SliceExactMonomPolyOps [in CoqApprox.poly_datatypes]
SliceExactPowDivOps [in CoqApprox.poly_datatypes]
SliceFullOps [in CoqApprox.poly_datatypes]
SliceMaskBaseOps [in CoqApprox.poly_datatypes]
SliceMonomPolyOps [in CoqApprox.poly_datatypes]
SlicePowDivOps [in CoqApprox.poly_datatypes]


T

TaylorModel [in CoqApprox.taylor_model_int_sharp]
TaylorModelFloat [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.MapFX [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.MapI [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.MapIF [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.RPAF [in CoqApprox.taylor_model_float_sharp]
TaylorModelFloat.TM [in CoqApprox.taylor_model_float_sharp]
TaylorModel.RPA [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TI [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TX [in CoqApprox.taylor_model_int_sharp]
TaylorPoly [in CoqApprox.taylor_poly]
TaylorPolyOps [in CoqApprox.taylor_poly]
TaylorPoly.Rec [in CoqApprox.taylor_poly]
TaylorRec [in CoqApprox.taylor_poly]
TMF [in CoqApprox.test_exp_sin]
TM_comp_0 [in CoqApprox.test_exp_sin]



Axiom Index

B

BaseOps.T [in CoqApprox.poly_datatypes]
BaseOps.tadd [in CoqApprox.poly_datatypes]
BaseOps.tmul [in CoqApprox.poly_datatypes]
BaseOps.tone [in CoqApprox.poly_datatypes]
BaseOps.topp [in CoqApprox.poly_datatypes]
BaseOps.tsub [in CoqApprox.poly_datatypes]
BaseOps.tzero [in CoqApprox.poly_datatypes]
BaseOps.U [in CoqApprox.poly_datatypes]


L

LinkIntX.link_tmul_tail [in CoqApprox.rpa_inst]
LinkIntX.link_tmul_trunc [in CoqApprox.rpa_inst]


P

PolyOps.teval [in CoqApprox.poly_datatypes]
PolyOps.tfold [in CoqApprox.poly_datatypes]
PolyOps.tfold_polyCons [in CoqApprox.poly_datatypes]
PolyOps.tfold_polyNil [in CoqApprox.poly_datatypes]
PolyOps.tlastN [in CoqApprox.poly_datatypes]
PolyOps.tlastN_spec [in CoqApprox.poly_datatypes]
PolyOps.tmul_tail [in CoqApprox.poly_datatypes]
PolyOps.tmul_trunc [in CoqApprox.poly_datatypes]
PolyOps.tnth [in CoqApprox.poly_datatypes]
PolyOps.tnth_set_nth_neq [in CoqApprox.poly_datatypes]
PolyOps.tnth_set_nth_eq [in CoqApprox.poly_datatypes]
PolyOps.tnth_out [in CoqApprox.poly_datatypes]
PolyOps.tnth_polyNil [in CoqApprox.poly_datatypes]
PolyOps.tnth_polyCons [in CoqApprox.poly_datatypes]
PolyOps.tnth_tadd [in CoqApprox.poly_datatypes]
PolyOps.tpolyCons [in CoqApprox.poly_datatypes]
PolyOps.tpolyNil [in CoqApprox.poly_datatypes]
PolyOps.tpoly_ind [in CoqApprox.poly_datatypes]
PolyOps.trecN [in CoqApprox.poly_datatypes]
PolyOps.trecN_spec [in CoqApprox.poly_datatypes]
PolyOps.trecN_spec0 [in CoqApprox.poly_datatypes]
PolyOps.trec1 [in CoqApprox.poly_datatypes]
PolyOps.trec1_spec [in CoqApprox.poly_datatypes]
PolyOps.trec1_spec0 [in CoqApprox.poly_datatypes]
PolyOps.trec2 [in CoqApprox.poly_datatypes]
PolyOps.trec2_spec [in CoqApprox.poly_datatypes]
PolyOps.trec2_spec1 [in CoqApprox.poly_datatypes]
PolyOps.trec2_spec0 [in CoqApprox.poly_datatypes]
PolyOps.tset_nth [in CoqApprox.poly_datatypes]
PolyOps.tsize [in CoqApprox.poly_datatypes]
PolyOps.tsize_set_nth [in CoqApprox.poly_datatypes]
PolyOps.tsize_polyNil [in CoqApprox.poly_datatypes]
PolyOps.tsize_polyCons [in CoqApprox.poly_datatypes]
PolyOps.tsize_tadd [in CoqApprox.poly_datatypes]
PolyOps.tsize_mul_tail [in CoqApprox.poly_datatypes]
PolyOps.tsize_mul_trunc [in CoqApprox.poly_datatypes]
PolyOps.tsize_trec2 [in CoqApprox.poly_datatypes]
PolyOps.tsize_trec1 [in CoqApprox.poly_datatypes]
PolyOps.tsize_trecN [in CoqApprox.poly_datatypes]


S

SliceExactBaseOps.big_distrr_spec [in CoqApprox.poly_datatypes]
SliceExactBaseOps.tadd_assoc [in CoqApprox.poly_datatypes]
SliceExactBaseOps.tadd_comm [in CoqApprox.poly_datatypes]
SliceExactBaseOps.tadd_zeror [in CoqApprox.poly_datatypes]
SliceExactBaseOps.tadd_zerol [in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_distrr [in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_distrl [in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_assoc [in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_comm [in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_oner [in CoqApprox.poly_datatypes]
SliceExactBaseOps.tmul_onel [in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_comm [in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_idemp [in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_mul_r [in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_mul_l [in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_add_r [in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask_add_l [in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask0mul_r [in CoqApprox.poly_datatypes]
SliceExactMaskBaseOps.mask0mul_l [in CoqApprox.poly_datatypes]
SliceExactMonomPolyOps.is_horner [in CoqApprox.poly_datatypes]
SliceExactMonomPolyOps.tmul_tail_nth [in CoqApprox.poly_datatypes]
SliceExactMonomPolyOps.tmul_trunc_nth [in CoqApprox.poly_datatypes]
SliceExactPowDivOps.tpow_opp [in CoqApprox.poly_datatypes]
SliceExactPowDivOps.tpow_S [in CoqApprox.poly_datatypes]
SliceExactPowDivOps.tpow_0 [in CoqApprox.poly_datatypes]
SliceFullOps.tcos [in CoqApprox.poly_datatypes]
SliceFullOps.texp [in CoqApprox.poly_datatypes]
SliceFullOps.tinvsqrt [in CoqApprox.poly_datatypes]
SliceFullOps.tnat [in CoqApprox.poly_datatypes]
SliceFullOps.tsin [in CoqApprox.poly_datatypes]
SliceFullOps.tsqrt [in CoqApprox.poly_datatypes]
SliceMaskBaseOps.tcst [in CoqApprox.poly_datatypes]
SliceMonomPolyOps.teval_polyNil [in CoqApprox.poly_datatypes]
SliceMonomPolyOps.teval_polyCons [in CoqApprox.poly_datatypes]
SlicePowDivOps.tdiv [in CoqApprox.poly_datatypes]
SlicePowDivOps.tinv [in CoqApprox.poly_datatypes]
SlicePowDivOps.tpower_int [in CoqApprox.poly_datatypes]
SlicePowDivOps.tsqr [in CoqApprox.poly_datatypes]


T

TaylorPolyOps.T_invsqrt [in CoqApprox.taylor_poly]
TaylorPolyOps.T_sqrt [in CoqApprox.taylor_poly]
TaylorPolyOps.T_cos [in CoqApprox.taylor_poly]
TaylorPolyOps.T_sin [in CoqApprox.taylor_poly]
TaylorPolyOps.T_exp [in CoqApprox.taylor_poly]
TaylorPolyOps.T_inv [in CoqApprox.taylor_poly]
TaylorPolyOps.T_var [in CoqApprox.taylor_poly]
TaylorPolyOps.T_cst [in CoqApprox.taylor_poly]



Variable Index

D

DefixN.F [in CoqApprox.basic_rec]
DefixN.F1 [in CoqApprox.basic_rec]
DefixN.init [in CoqApprox.basic_rec]
DefixN.N [in CoqApprox.basic_rec]
DefixN.T [in CoqApprox.basic_rec]
Defix1.a0 [in CoqApprox.basic_rec]
Defix1.d [in CoqApprox.basic_rec]
Defix1.F [in CoqApprox.basic_rec]
Defix1.T [in CoqApprox.basic_rec]
Defix2.a0 [in CoqApprox.basic_rec]
Defix2.a1 [in CoqApprox.basic_rec]
Defix2.d [in CoqApprox.basic_rec]
Defix2.F [in CoqApprox.basic_rec]
Defix2.T [in CoqApprox.basic_rec]


F

Fold.A [in CoqApprox.seq_compl]
Fold.B [in CoqApprox.seq_compl]
Fold.f [in CoqApprox.seq_compl]


H

Head_Last.d [in CoqApprox.seq_compl]
Head_Last.T [in CoqApprox.seq_compl]


M

Map2.A [in CoqApprox.seq_compl]
Map2.B [in CoqApprox.seq_compl]
Map2.C [in CoqApprox.seq_compl]
Map2.f [in CoqApprox.seq_compl]


N

NaryTupleCast.T [in CoqApprox.nary_tuple]
NaryTupleMap.f [in CoqApprox.nary_tuple]
NaryTupleMap.rT [in CoqApprox.nary_tuple]
NaryTupleMap.T [in CoqApprox.nary_tuple]
NaryTupleMkNat.f [in CoqApprox.nary_tuple]
NaryTupleMkNat.n [in CoqApprox.nary_tuple]
NaryTupleMkNat.U [in CoqApprox.nary_tuple]
NaryTupleMk.f [in CoqApprox.nary_tuple]
NaryTupleMk.n [in CoqApprox.nary_tuple]
NaryTupleMk.U [in CoqApprox.nary_tuple]
NaryTupleSeq.n [in CoqApprox.nary_tuple]
NaryTupleSeq.T [in CoqApprox.nary_tuple]
NaryTuple.n [in CoqApprox.nary_tuple]
NaryTuple.T [in CoqApprox.nary_tuple]
NaryTuple1.n [in CoqApprox.nary_tuple]
NaryTuple1.T [in CoqApprox.nary_tuple]
NDerive.dom [in CoqApprox.xreal_ssr_compat]
NDerive.Hder [in CoqApprox.xreal_ssr_compat]
NDerive.Hdif [in CoqApprox.xreal_ssr_compat]
NDerive.Hdom [in CoqApprox.xreal_ssr_compat]
NDerive.n [in CoqApprox.xreal_ssr_compat]
NDerive.X [in CoqApprox.xreal_ssr_compat]
NDerive.XD [in CoqApprox.xreal_ssr_compat]
NDerive.XD0_Xnan [in CoqApprox.xreal_ssr_compat]


P

ProofN.F [in CoqApprox.basic_rec]
ProofN.init [in CoqApprox.basic_rec]
ProofN.N [in CoqApprox.basic_rec]
ProofN.T [in CoqApprox.basic_rec]


S

SeqPolyMonomUp.PrecIsPropagated.u [in CoqApprox.poly_inst_seq]


T

takeN_lastN.d [in CoqApprox.nary_tuple]
takeN_lastN.T [in CoqApprox.nary_tuple]
Take.T [in CoqApprox.seq_compl]
TaylorLagrange.a [in CoqApprox.taylor_thm]
TaylorLagrange.b [in CoqApprox.taylor_thm]
TaylorLagrange.CorTL.derivable_pt_lim_Dp [in CoqApprox.taylor_thm]
TaylorLagrange.D [in CoqApprox.taylor_thm]
TaylorLagrange.n [in CoqApprox.taylor_thm]
TaylorLagrange.TL.c [in CoqApprox.taylor_thm]
TaylorLagrange.TL.continuity_pt_Dp [in CoqApprox.taylor_thm]
TaylorLagrange.TL.derivable_pt_lim_Dp [in CoqApprox.taylor_thm]
TaylorLagrange.TL.g [in CoqApprox.taylor_thm]
TaylorLagrange.TL.Hx [in CoqApprox.taylor_thm]
TaylorLagrange.TL.Hx0 [in CoqApprox.taylor_thm]
TaylorLagrange.TL.x [in CoqApprox.taylor_thm]
TaylorLagrange.TL.x0 [in CoqApprox.taylor_thm]
TaylorModel.PrecArgument.prec [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.F0 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.F0_contains [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.GenericProof.IP [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.GenericProof.XP [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec1_correct.F_rec [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec1_correct.XF_rec [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.F_rec [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.XF_rec [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.F1_contains [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.XDn_1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.F1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.rec2_correct.XF1 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.XDn [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.XF0 [in CoqApprox.taylor_model_int_sharp]
TaylorModel.PrecArgument.ProofOfRec.XF0_Xnan [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TaylorModel.M [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TaylorModel.prec [in CoqApprox.taylor_model_int_sharp]
TaylorModel.TaylorModel.Tcoeffs [in CoqApprox.taylor_model_int_sharp]
TaylorPoly.PrecIsPropagated.u [in CoqApprox.taylor_poly]
TaylorRec.PrecIsPropagated.u [in CoqApprox.taylor_poly]
TestN.F [in CoqApprox.basic_rec]
TestN.FibN [in CoqApprox.basic_rec]
TestN.FibNc [in CoqApprox.basic_rec]
TestN.FibNc' [in CoqApprox.basic_rec]
TestN.FibNs [in CoqApprox.basic_rec]
TestN.FibNs' [in CoqApprox.basic_rec]
TestN.FibN' [in CoqApprox.basic_rec]
TestN.Fib2 [in CoqApprox.basic_rec]
Test1.fact [in CoqApprox.basic_rec]
Test1.factz_rec [in CoqApprox.basic_rec]
Test1.fact_rec [in CoqApprox.basic_rec]
Test1.n_rec [in CoqApprox.basic_rec]
Test2.fibz_rec [in CoqApprox.basic_rec]
Test2.foo2 [in CoqApprox.basic_rec]
Test2.foo2_rec [in CoqApprox.basic_rec]
Tuplify.T [in CoqApprox.nary_tuple]



Library Index

B

basic_rec


C

coeff_inst


D

derive_compl


I

interval_compl


N

nary_tuple


P

poly_inst_seq
poly_datatypes


R

rpa_inst
Rstruct


S

seq_compl


T

taylor_poly
taylor_model_float_sharp
taylor_model_int_sharp
taylor_thm
test_exp_sin


X

xreal_ssr_compat



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1154 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (11 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (8 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (451 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (44 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (25 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (8 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (5 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (33 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (272 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (77 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (95 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (105 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (16 entries)

This page has been generated by coqdoc | Return to the CoqApprox web page