| 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 | (1493 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 | (7 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 | (116 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 | (37 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 | (335 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 | (1 entry) |
| 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 | (25 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 | (10 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 | (27 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 | (9 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 | (84 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 | (842 entries) |
Global Index
A
about_reptype_ftype [lemma, in LAProof.C.spec_densemat]about_the_ctype [lemma, in LAProof.C.spec_densemat]
abs_le_rel [lemma, in LAProof.accuracy_proofs.common]
alloc [library]
allocASI [definition, in LAProof.C.spec_alloc]
allocVSU [definition, in LAProof.C.verif_alloc]
alloc_internal_specs [definition, in LAProof.C.verif_alloc]
alloc_imported_specs [definition, in LAProof.C.verif_alloc]
alloc_E [definition, in LAProof.C.verif_alloc]
all_nth_eq [lemma, in LAProof.C.floatlib]
B
backward_subst [definition, in LAProof.C.matrix_model]backward_subst_step [definition, in LAProof.C.matrix_model]
bandmat [library]
Beq_dec_t [definition, in LAProof.accuracy_proofs.common]
BFMA_correct [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BFMA_finite_e [lemma, in LAProof.accuracy_proofs.float_acc_lems]
Bfma_mult_0R [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BFMA_eq [lemma, in LAProof.C.spec_sparse]
bfVNRM1 [lemma, in LAProof.accuracy_proofs.vecnorm_acc]
bfVNRM2 [lemma, in LAProof.accuracy_proofs.vecnorm_acc]
big_max_mul [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
big_mul [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
blocksolve_spec [definition, in LAProof.C.spec_densemat]
BMINUS_accurate' [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BMINUS_accurate [lemma, in LAProof.accuracy_proofs.float_acc_lems]
Bminus_no_overflow [definition, in LAProof.accuracy_proofs.float_acc_lems]
BMINUS_finite_sub [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BMINUS_neg_zero [lemma, in LAProof.accuracy_proofs.sum_model]
BMULT_correct [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BMULT_finite_e [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BMULT_accurate' [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BMULT_accurate [lemma, in LAProof.accuracy_proofs.float_acc_lems]
Bmult_no_overflow [definition, in LAProof.accuracy_proofs.float_acc_lems]
Bmult_0R [lemma, in LAProof.accuracy_proofs.float_acc_lems]
body_crs_matrix_vector_multiply [lemma, in LAProof.C.verif_sparse]
body_double_clear [lemma, in LAProof.C.verif_alloc]
body_int_calloc [lemma, in LAProof.C.verif_alloc]
body_double_calloc [lemma, in LAProof.C.verif_alloc]
body_surely_malloc [lemma, in LAProof.C.verif_alloc]
body_exit [axiom, in LAProof.C.verif_alloc]
body_densemat_dotprod [lemma, in LAProof.C.verif_densemat_mult]
body_densematn_dotprod [lemma, in LAProof.C.verif_densemat_mult]
body_densemat_mult [lemma, in LAProof.C.verif_densemat_mult]
body_densematn_mult [lemma, in LAProof.C.verif_densemat_mult]
body_cholesky [lemma, in LAProof.C.verif_cholesky]
body_densemat_csolve [lemma, in LAProof.C.verif_densemat_cholesky]
body_densematn_csolve [lemma, in LAProof.C.verif_densemat_cholesky]
body_densemat_cfactor [lemma, in LAProof.C.verif_densemat_cholesky]
body_densematn_cfactor [lemma, in LAProof.C.verif_densemat_cholesky]
body_densemat_norm [lemma, in LAProof.C.verif_densemat]
body_densemat_norm2 [lemma, in LAProof.C.verif_densemat]
body_data_norm [lemma, in LAProof.C.verif_densemat]
body_data_norm2 [lemma, in LAProof.C.verif_densemat]
body_densemat_addto [lemma, in LAProof.C.verif_densemat]
body_densematn_addto [lemma, in LAProof.C.verif_densemat]
body_densemat_set [lemma, in LAProof.C.verif_densemat]
body_densematn_set [lemma, in LAProof.C.verif_densemat]
body_densemat_get [lemma, in LAProof.C.verif_densemat]
body_densematn_get [lemma, in LAProof.C.verif_densemat]
body_densemat_clear [lemma, in LAProof.C.verif_densemat]
body_densematn_clear [lemma, in LAProof.C.verif_densemat]
body_densemat_free [lemma, in LAProof.C.verif_densemat]
body_densemat_malloc [lemma, in LAProof.C.verif_densemat]
body_crs_matrix_vector_multiply_byrows [lemma, in LAProof.C.verif_sparse_byrows]
body_crs_row_vector_multiply [lemma, in LAProof.C.verif_sparse_byrows]
body_crs_matrix_rows [lemma, in LAProof.C.verif_sparse_byrows]
BPLUS_correct [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BPLUS_accurate' [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BPLUS_accurate [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BPLUS_B2R_zero [lemma, in LAProof.accuracy_proofs.float_acc_lems]
Bplus_no_overflow [definition, in LAProof.accuracy_proofs.float_acc_lems]
BPLUS_finite_e [lemma, in LAProof.accuracy_proofs.float_acc_lems]
Bplus_0R [lemma, in LAProof.accuracy_proofs.float_acc_lems]
BPLUS_comm [lemma, in LAProof.accuracy_proofs.sum_model]
BPLUS_neg_zero [lemma, in LAProof.accuracy_proofs.sum_model]
bpow_fprec_lb [lemma, in LAProof.accuracy_proofs.fma_is_finite]
bpow_femax_lb [lemma, in LAProof.accuracy_proofs.fma_is_finite]
bSUM [lemma, in LAProof.accuracy_proofs.sum_acc]
C
change_composite_env_alloc' [instance, in LAProof.C.densemat_lemmas]change_composite_env_alloc [instance, in LAProof.C.densemat_lemmas]
check_densemat_layout [lemma, in LAProof.C.spec_densemat]
cholesky [library]
cholesky_jik_upto_newrow [lemma, in LAProof.C.matrix_model]
cholesky_jik_upto_zero [lemma, in LAProof.C.matrix_model]
cholesky_jik_ij' [definition, in LAProof.C.matrix_model]
cholesky_jik_upto [definition, in LAProof.C.matrix_model]
cholesky_jik_spec [definition, in LAProof.C.matrix_model]
cholesky_jik_ij [definition, in LAProof.C.matrix_model]
cholesky_spec [definition, in LAProof.C.verif_cholesky]
cholesky_jik_upto [definition, in LAProof.C.verif_cholesky]
cholesky_jik_spec [definition, in LAProof.C.verif_cholesky]
cholesky_jik_ij [definition, in LAProof.C.verif_cholesky]
column_major [definition, in LAProof.C.spec_densemat]
column_major_const [lemma, in LAProof.C.densemat_lemmas]
combine_split [lemma, in LAProof.accuracy_proofs.fma_is_finite]
common [library]
composites [definition, in LAProof.C.sparse]
composites [definition, in LAProof.C.densemat]
composites [definition, in LAProof.C.cholesky]
composites [definition, in LAProof.C.bandmat]
composites [definition, in LAProof.C.alloc]
CompSpecs [instance, in LAProof.C.spec_densemat]
CompSpecs [instance, in LAProof.C.spec_alloc]
CompSpecs [instance, in LAProof.C.verif_cholesky]
CompSpecs [instance, in LAProof.C.spec_sparse]
crazy [definition, in LAProof.accuracy_proofs.mv_mathcomp]
crs_multiply_loop_body [lemma, in LAProof.C.verif_sparse]
crs_matrix_vector_multiply_spec [definition, in LAProof.C.spec_sparse]
crs_matrix_vector_multiply_byrows_spec [definition, in LAProof.C.spec_sparse]
crs_row_vector_multiply_spec [definition, in LAProof.C.spec_sparse]
crs_matrix_rows_spec [definition, in LAProof.C.spec_sparse]
crs_rep [definition, in LAProof.C.spec_sparse]
crs_row_rep_property [lemma, in LAProof.C.sparse_model]
crs_row_rep_col_range [lemma, in LAProof.C.sparse_model]
crs_row_rep_cols_nonneg [lemma, in LAProof.C.sparse_model]
crs_rep_matrix_cols [lemma, in LAProof.C.sparse_model]
crs_rep_aux [definition, in LAProof.C.sparse_model]
crs_row_rep_sind [definition, in LAProof.C.sparse_model]
crs_row_rep_ind [definition, in LAProof.C.sparse_model]
crs_row_rep_val [constructor, in LAProof.C.sparse_model]
crs_row_rep_zero [constructor, in LAProof.C.sparse_model]
crs_row_rep_nil [constructor, in LAProof.C.sparse_model]
crs_row_rep [inductive, in LAProof.C.sparse_model]
ctype_of_the_type [lemma, in LAProof.C.spec_densemat]
ctype_of_type [definition, in LAProof.C.spec_densemat]
D
D [abbreviation, in LAProof.accuracy_proofs.dot_acc]D [abbreviation, in LAProof.accuracy_proofs.float_acc_lems]
D [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
D [abbreviation, in LAProof.accuracy_proofs.common]
D [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
D [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
D [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
D [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
D [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
D [abbreviation, in LAProof.accuracy_proofs.sum_acc]
data_norm_spec [definition, in LAProof.C.spec_densemat]
data_norm2_spec [definition, in LAProof.C.spec_densemat]
default_abs_ge_0 [lemma, in LAProof.accuracy_proofs.common]
default_abs_gt_0 [lemma, in LAProof.accuracy_proofs.common]
default_rel_plus_1_ge_1' [lemma, in LAProof.accuracy_proofs.common]
default_rel_plus_1_gt_0 [lemma, in LAProof.accuracy_proofs.common]
default_rel_plus_1_gt_1 [lemma, in LAProof.accuracy_proofs.common]
default_rel_plus_0_ge_1 [lemma, in LAProof.accuracy_proofs.common]
default_rel_plus_1_ge_1 [lemma, in LAProof.accuracy_proofs.common]
default_rel_ge_0 [lemma, in LAProof.accuracy_proofs.common]
default_rel_gt_0 [lemma, in LAProof.accuracy_proofs.common]
default_rel_sep_0 [lemma, in LAProof.accuracy_proofs.common]
default_abs [definition, in LAProof.accuracy_proofs.common]
default_rel [definition, in LAProof.accuracy_proofs.common]
default_rel_ub [lemma, in LAProof.accuracy_proofs.fma_is_finite]
default_abs_ub [lemma, in LAProof.accuracy_proofs.fma_is_finite]
defualt_abs_le_fmax [lemma, in LAProof.accuracy_proofs.fma_is_finite]
densemat [definition, in LAProof.C.spec_densemat]
densemat [library]
densematASI [definition, in LAProof.C.spec_densemat]
densematn [definition, in LAProof.C.spec_densemat]
densematn_cfactor_outer_spec [definition, in LAProof.C.spec_densemat]
densematn_cfactor_block_spec [definition, in LAProof.C.spec_densemat]
densematn_lusolveT_spec [definition, in LAProof.C.spec_densemat]
densematn_lufactor_spec [definition, in LAProof.C.spec_densemat]
densematn_lusolve_spec [definition, in LAProof.C.spec_densemat]
densematn_print_spec [definition, in LAProof.C.spec_densemat]
densematn_lujac_spec [definition, in LAProof.C.spec_densemat]
densematn_mult_spec [definition, in LAProof.C.spec_densemat]
densematn_dotprod_spec [definition, in LAProof.C.spec_densemat]
densematn_csolve_spec [definition, in LAProof.C.spec_densemat]
densematn_cfactor_spec [definition, in LAProof.C.spec_densemat]
densematn_addto_spec [definition, in LAProof.C.spec_densemat]
densematn_set_spec [definition, in LAProof.C.spec_densemat]
densematn_get_spec [definition, in LAProof.C.spec_densemat]
densematn_clear_spec [definition, in LAProof.C.spec_densemat]
densematn_valid_pointer [lemma, in LAProof.C.spec_densemat]
densematn_local_facts [definition, in LAProof.C.spec_densemat]
densematVSU [definition, in LAProof.C.VSU_densemat]
densemat_lusolveT_spec [definition, in LAProof.C.spec_densemat]
densemat_lufactor_spec [definition, in LAProof.C.spec_densemat]
densemat_lusolve_spec [definition, in LAProof.C.spec_densemat]
densemat_print_spec [definition, in LAProof.C.spec_densemat]
densemat_lujac_spec [definition, in LAProof.C.spec_densemat]
densemat_mult_spec [definition, in LAProof.C.spec_densemat]
densemat_dotprod_spec [definition, in LAProof.C.spec_densemat]
densemat_csolve_spec [definition, in LAProof.C.spec_densemat]
densemat_cfactor_spec [definition, in LAProof.C.spec_densemat]
densemat_norm_spec [definition, in LAProof.C.spec_densemat]
densemat_norm2_spec [definition, in LAProof.C.spec_densemat]
densemat_addto_spec [definition, in LAProof.C.spec_densemat]
densemat_set_spec [definition, in LAProof.C.spec_densemat]
densemat_get_spec [definition, in LAProof.C.spec_densemat]
densemat_clear_spec [definition, in LAProof.C.spec_densemat]
densemat_free_spec [definition, in LAProof.C.spec_densemat]
densemat_malloc_spec [definition, in LAProof.C.spec_densemat]
densemat_valid_pointer [lemma, in LAProof.C.spec_densemat]
densemat_local_facts [definition, in LAProof.C.spec_densemat]
densemat_data_offset [definition, in LAProof.C.spec_densemat]
densemat_t [definition, in LAProof.C.spec_densemat]
densemat_field_compat0 [lemma, in LAProof.C.densemat_lemmas]
densemat_internal_specs [definition, in LAProof.C.densemat_lemmas]
densemat_imported_specs [definition, in LAProof.C.densemat_lemmas]
densemat_E [definition, in LAProof.C.densemat_lemmas]
densemat_lemmas [library]
done_to_n [definition, in LAProof.C.verif_cholesky]
done_to_ij [definition, in LAProof.C.verif_cholesky]
dotprod [definition, in LAProof.accuracy_proofs.dotprod_model]
dotprod [definition, in LAProof.C.floatlib]
dotprodF [definition, in LAProof.accuracy_proofs.dotprod_model]
DotProdFloat [section, in LAProof.accuracy_proofs.dotprod_model]
DotProdFloat.NAN [variable, in LAProof.accuracy_proofs.dotprod_model]
DotProdFloat.t [variable, in LAProof.accuracy_proofs.dotprod_model]
DotProdFMA [section, in LAProof.accuracy_proofs.dotprod_model]
DotProdFMA.NAN [variable, in LAProof.accuracy_proofs.dotprod_model]
DotProdFMA.t [variable, in LAProof.accuracy_proofs.dotprod_model]
dotprodF_rel_fold_right [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprodR [definition, in LAProof.accuracy_proofs.dotprod_model]
dotprodR_rel_bound'' [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprodR_rel_bound' [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprodR_rev [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprodR_rel_inj [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprodR_rel [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprodR_nil_r [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprodR_nil_l [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprod_forward_error [lemma, in LAProof.accuracy_proofs.dot_acc]
dotprod_mixed_error [lemma, in LAProof.accuracy_proofs.dot_acc]
dotprod_mixed_error_rel [lemma, in LAProof.accuracy_proofs.dot_acc_lemmas]
dotprod_forward_error_rel [lemma, in LAProof.accuracy_proofs.dot_acc_lemmas]
dotprod_rel_R_exists_fma [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprod_rel_R_exists [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprod_rel_dotprod_any [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprod_any_sind [definition, in LAProof.accuracy_proofs.dotprod_model]
dotprod_any_ind [definition, in LAProof.accuracy_proofs.dotprod_model]
Dotprod_Any_Some [constructor, in LAProof.accuracy_proofs.dotprod_model]
Dotprod_Any_None [constructor, in LAProof.accuracy_proofs.dotprod_model]
dotprod_any [inductive, in LAProof.accuracy_proofs.dotprod_model]
dotprod_any'_sind [definition, in LAProof.accuracy_proofs.dotprod_model]
dotprod_any'_ind [definition, in LAProof.accuracy_proofs.dotprod_model]
Dotprod_Any_perm [constructor, in LAProof.accuracy_proofs.dotprod_model]
Dotprod_Any_split [constructor, in LAProof.accuracy_proofs.dotprod_model]
Dotprod_Any_1 [constructor, in LAProof.accuracy_proofs.dotprod_model]
dotprod_any' [inductive, in LAProof.accuracy_proofs.dotprod_model]
dotprod_single [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprod_nil_r [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprod_nil_l [lemma, in LAProof.accuracy_proofs.dotprod_model]
dotprod_congr [lemma, in LAProof.C.floatlib]
dotprod_model [library]
dot_prod_rel_nnzR [lemma, in LAProof.accuracy_proofs.dotprod_model]
dot_prod_zip_map_Rmult [lemma, in LAProof.accuracy_proofs.dotprod_model]
dot_prod_sum_rel_R_Rabs [lemma, in LAProof.accuracy_proofs.dotprod_model]
dot_prod_rel_sind [definition, in LAProof.accuracy_proofs.dotprod_model]
dot_prod_rel_ind [definition, in LAProof.accuracy_proofs.dotprod_model]
dot_prod_rel_cons [constructor, in LAProof.accuracy_proofs.dotprod_model]
dot_prod_rel_nil [constructor, in LAProof.accuracy_proofs.dotprod_model]
dot_prod_rel [inductive, in LAProof.accuracy_proofs.dotprod_model]
dot_acc [library]
dot_acc_lemmas [library]
double_clear_spec [definition, in LAProof.C.spec_alloc]
double_calloc_spec [definition, in LAProof.C.spec_alloc]
drop_sublist [lemma, in LAProof.C.densemat_lemmas]
d_le_g_1 [lemma, in LAProof.accuracy_proofs.common]
d_le_g [lemma, in LAProof.accuracy_proofs.common]
E
E [abbreviation, in LAProof.accuracy_proofs.dot_acc]E [abbreviation, in LAProof.accuracy_proofs.float_acc_lems]
E [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
E [abbreviation, in LAProof.accuracy_proofs.common]
E [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
E [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
E [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
E [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
E [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
eq_in_subrange [lemma, in LAProof.C.matrix_model]
exists_mx [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
exit_spec [definition, in LAProof.C.spec_alloc]
export [library]
e_le_g1 [lemma, in LAProof.accuracy_proofs.common]
F
F [module, in LAProof.accuracy_proofs.mv_mathcomp]F [module, in LAProof.C.spec_densemat]
Faddmx_mixed_error [lemma, in LAProof.accuracy_proofs.vec_op_acc]
finite_norm2_e [lemma, in LAProof.C.floatlib]
finite_dotprod_e [lemma, in LAProof.C.floatlib]
finite_sum_from_bounded [lemma, in LAProof.accuracy_proofs.fma_is_finite]
firstn_seq [lemma, in LAProof.C.densemat_lemmas]
flip_Rplus [lemma, in LAProof.accuracy_proofs.dotprod_model]
floatlib [library]
float_acc_lems [library]
fmax [definition, in LAProof.accuracy_proofs.fma_is_finite]
fma_accurate' [lemma, in LAProof.accuracy_proofs.float_acc_lems]
fma_accurate [lemma, in LAProof.accuracy_proofs.float_acc_lems]
fma_no_overflow [definition, in LAProof.accuracy_proofs.float_acc_lems]
fma_sparse_dotprod_forward_error [lemma, in LAProof.accuracy_proofs.fma_dot_acc]
fma_dotprod_forward_error [lemma, in LAProof.accuracy_proofs.fma_dot_acc]
fma_dotprod_mixed_error [lemma, in LAProof.accuracy_proofs.fma_dot_acc]
fma_dotprod_mixed_error_rel [lemma, in LAProof.accuracy_proofs.dot_acc_lemmas]
fma_dotprod_forward_error_rel [lemma, in LAProof.accuracy_proofs.dot_acc_lemmas]
fma_dot_prod_rel_nnzR [lemma, in LAProof.accuracy_proofs.dotprod_model]
fma_dot_prod_rel_fold_right [lemma, in LAProof.accuracy_proofs.dotprod_model]
fma_dot_prod_rel_sind [definition, in LAProof.accuracy_proofs.dotprod_model]
fma_dot_prod_rel_ind [definition, in LAProof.accuracy_proofs.dotprod_model]
fma_dot_prod_rel_cons [constructor, in LAProof.accuracy_proofs.dotprod_model]
fma_dot_prod_rel_nil [constructor, in LAProof.accuracy_proofs.dotprod_model]
fma_dot_prod_rel [inductive, in LAProof.accuracy_proofs.dotprod_model]
fma_dotprod [definition, in LAProof.accuracy_proofs.dotprod_model]
fma_dot_acc [library]
fma_is_finite [library]
fold_crs_rep [lemma, in LAProof.C.verif_sparse_byrows]
fold_left_preserves [lemma, in LAProof.C.densemat_lemmas]
ForwardError [section, in LAProof.accuracy_proofs.dot_acc]
ForwardError [section, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardErrorRel1 [section, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel1.NAN [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel1.t [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2 [section, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.fp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.Hfin [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.Hfp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.Hra [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.Hrp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.NAN [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.rp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.rp_abs [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.t [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.vF [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardError.Hfin [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.Hfin [variable, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.Hlen [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.Hlen [variable, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.NAN [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.NAN [variable, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.t [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.t [variable, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.v1 [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.v1 [variable, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.v2 [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.v2 [variable, in LAProof.accuracy_proofs.fma_dot_acc]
forward_subst [definition, in LAProof.C.matrix_model]
forward_subst_step [definition, in LAProof.C.matrix_model]
frobenius_norm [definition, in LAProof.C.spec_densemat]
frobenius_norm2 [definition, in LAProof.C.spec_densemat]
FR2 [definition, in LAProof.accuracy_proofs.dotprod_model]
Fscalemx_mixed_error [lemma, in LAProof.accuracy_proofs.vec_op_acc]
fSUM [lemma, in LAProof.accuracy_proofs.sum_acc]
Fsum_forward_error [lemma, in LAProof.accuracy_proofs.sum_acc]
Fsum_backward_error [lemma, in LAProof.accuracy_proofs.sum_acc]
FT2R_Zconst_0 [lemma, in LAProof.accuracy_proofs.float_acc_lems]
FT2R_pos_zero [lemma, in LAProof.accuracy_proofs.float_acc_lems]
FT2R_neg_zero [lemma, in LAProof.accuracy_proofs.float_acc_lems]
FT2R_FR2 [lemma, in LAProof.accuracy_proofs.dotprod_model]
fun_bound_pos [lemma, in LAProof.accuracy_proofs.fma_is_finite]
fun_bnd_le [lemma, in LAProof.accuracy_proofs.fma_is_finite]
fun_bnd_pos_1 [lemma, in LAProof.accuracy_proofs.fma_is_finite]
fun_bnd [definition, in LAProof.accuracy_proofs.fma_is_finite]
f_crs_matrix_rows [definition, in LAProof.C.sparse]
f_crs_matrix_vector_multiply [definition, in LAProof.C.sparse]
f_crs_matrix_vector_multiply_byrows [definition, in LAProof.C.sparse]
f_crs_row_vector_multiply [definition, in LAProof.C.sparse]
f_densemat_mult [definition, in LAProof.C.densemat]
f_densematn_mult [definition, in LAProof.C.densemat]
f_densemat_dotprod [definition, in LAProof.C.densemat]
f_densematn_dotprod [definition, in LAProof.C.densemat]
f_densemat_norm [definition, in LAProof.C.densemat]
f_densemat_norm2 [definition, in LAProof.C.densemat]
f_data_norm [definition, in LAProof.C.densemat]
f_data_norm2 [definition, in LAProof.C.densemat]
f_densemat_lujac [definition, in LAProof.C.densemat]
f_densemat_lusolveT [definition, in LAProof.C.densemat]
f_densemat_lusolve [definition, in LAProof.C.densemat]
f_densemat_lufactor [definition, in LAProof.C.densemat]
f_densematn_lujac [definition, in LAProof.C.densemat]
f_densematn_lusolveT [definition, in LAProof.C.densemat]
f_densematn_lusolve [definition, in LAProof.C.densemat]
f_densematn_lufactor [definition, in LAProof.C.densemat]
f_densemat_csolve [definition, in LAProof.C.densemat]
f_densematn_csolve [definition, in LAProof.C.densemat]
f_densemat_cfactor [definition, in LAProof.C.densemat]
f_densematn_cfactor_block [definition, in LAProof.C.densemat]
f_subtractoff [definition, in LAProof.C.densemat]
f_blocksolve [definition, in LAProof.C.densemat]
f_densematn_cfactor_outer [definition, in LAProof.C.densemat]
f_densematn_cfactor [definition, in LAProof.C.densemat]
f_densemat_print [definition, in LAProof.C.densemat]
f_densematn_print [definition, in LAProof.C.densemat]
f_densemat_addto [definition, in LAProof.C.densemat]
f_densemat_set [definition, in LAProof.C.densemat]
f_densemat_get [definition, in LAProof.C.densemat]
f_densematn_addto [definition, in LAProof.C.densemat]
f_densematn_set [definition, in LAProof.C.densemat]
f_densematn_get [definition, in LAProof.C.densemat]
f_densemat_clear [definition, in LAProof.C.densemat]
f_densematn_clear [definition, in LAProof.C.densemat]
f_densemat_free [definition, in LAProof.C.densemat]
f_densemat_malloc [definition, in LAProof.C.densemat]
f_cholesky [definition, in LAProof.C.cholesky]
f_bandmat_norm [definition, in LAProof.C.bandmat]
f_bandmat_norm2 [definition, in LAProof.C.bandmat]
f_bandmat_solve [definition, in LAProof.C.bandmat]
f_bandmat_factor [definition, in LAProof.C.bandmat]
f_bandmat_print [definition, in LAProof.C.bandmat]
f_dense_to_band [definition, in LAProof.C.bandmat]
f_bandmat_addto [definition, in LAProof.C.bandmat]
f_bandmat_set [definition, in LAProof.C.bandmat]
f_bandmat_get [definition, in LAProof.C.bandmat]
f_bandmatn_addto [definition, in LAProof.C.bandmat]
f_bandmatn_set [definition, in LAProof.C.bandmat]
f_bandmatn_get [definition, in LAProof.C.bandmat]
f_bandmat_clear [definition, in LAProof.C.bandmat]
f_bandmatn_clear [definition, in LAProof.C.bandmat]
f_bandmat_free [definition, in LAProof.C.bandmat]
f_bandmat_malloc [definition, in LAProof.C.bandmat]
f_int_calloc [definition, in LAProof.C.alloc]
f_double_calloc [definition, in LAProof.C.alloc]
f_double_clear [definition, in LAProof.C.alloc]
f_surely_malloc [definition, in LAProof.C.alloc]
F.addmx [definition, in LAProof.accuracy_proofs.mv_mathcomp]
F.dotprod [definition, in LAProof.accuracy_proofs.mv_mathcomp]
F.dotprod_dotprodF [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
F.finitemx [definition, in LAProof.accuracy_proofs.mv_mathcomp]
F.finitemx_scalemx_e [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
F.finitemx_addmx_e [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
F.mulmx [definition, in LAProof.accuracy_proofs.mv_mathcomp]
F.mulmx_dotprodF [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
F.mulmx_row [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
F.scalemx [definition, in LAProof.accuracy_proofs.mv_mathcomp]
F.sum [definition, in LAProof.accuracy_proofs.mv_mathcomp]
F.sum_sumF [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
F.WithNAN [section, in LAProof.accuracy_proofs.mv_mathcomp]
F.WithNAN.NAN [variable, in LAProof.accuracy_proofs.mv_mathcomp]
F.WithNAN.t [variable, in LAProof.accuracy_proofs.mv_mathcomp]
G
g [abbreviation, in LAProof.accuracy_proofs.gemm_acc]g [abbreviation, in LAProof.accuracy_proofs.dot_acc]
g [abbreviation, in LAProof.accuracy_proofs.dot_acc]
g [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
g [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
g [definition, in LAProof.accuracy_proofs.common]
g [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g [abbreviation, in LAProof.accuracy_proofs.sum_acc]
g [abbreviation, in LAProof.accuracy_proofs.vec_op_acc]
g [abbreviation, in LAProof.accuracy_proofs.vecnorm_acc]
g [abbreviation, in LAProof.accuracy_proofs.vecnorm_acc]
g [abbreviation, in LAProof.accuracy_proofs.gemv_acc]
GEMM_error [lemma, in LAProof.accuracy_proofs.gemm_acc]
gemm_acc [library]
gemv_error [lemma, in LAProof.accuracy_proofs.vec_op_acc]
gemv_acc [library]
generic_round_property [lemma, in LAProof.accuracy_proofs.float_acc_lems]
GenFloat [section, in LAProof.accuracy_proofs.float_acc_lems]
GenFloat.NAN [variable, in LAProof.accuracy_proofs.float_acc_lems]
GenFloat.t [variable, in LAProof.accuracy_proofs.float_acc_lems]
global_definitions [definition, in LAProof.C.sparse]
global_definitions [definition, in LAProof.C.densemat]
global_definitions [definition, in LAProof.C.cholesky]
global_definitions [definition, in LAProof.C.bandmat]
global_definitions [definition, in LAProof.C.alloc]
Gprog [definition, in LAProof.C.verif_alloc]
Gprog [definition, in LAProof.C.verif_cholesky]
Gprog [definition, in LAProof.C.spec_sparse]
Gprog [definition, in LAProof.C.densemat_lemmas]
g_pos [lemma, in LAProof.accuracy_proofs.common]
g1 [abbreviation, in LAProof.accuracy_proofs.gemm_acc]
g1 [abbreviation, in LAProof.accuracy_proofs.dot_acc]
g1 [abbreviation, in LAProof.accuracy_proofs.dot_acc]
g1 [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
g1 [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
g1 [definition, in LAProof.accuracy_proofs.common]
g1 [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [abbreviation, in LAProof.accuracy_proofs.vec_op_acc]
g1 [abbreviation, in LAProof.accuracy_proofs.vecnorm_acc]
g1 [abbreviation, in LAProof.accuracy_proofs.gemv_acc]
g1n_lt_g1Sn [lemma, in LAProof.accuracy_proofs.common]
g1n_le_g1Sn' [lemma, in LAProof.accuracy_proofs.common]
g1n_le_g1Sn [lemma, in LAProof.accuracy_proofs.common]
g1_pos [lemma, in LAProof.accuracy_proofs.common]
I
index_ord_enum [lemma, in LAProof.accuracy_proofs.mv_mathcomp]Info [module, in LAProof.C.sparse]
Info [module, in LAProof.C.densemat]
Info [module, in LAProof.C.cholesky]
Info [module, in LAProof.C.bandmat]
Info [module, in LAProof.C.alloc]
Info.abi [definition, in LAProof.C.sparse]
Info.abi [definition, in LAProof.C.densemat]
Info.abi [definition, in LAProof.C.cholesky]
Info.abi [definition, in LAProof.C.bandmat]
Info.abi [definition, in LAProof.C.alloc]
Info.arch [definition, in LAProof.C.sparse]
Info.arch [definition, in LAProof.C.densemat]
Info.arch [definition, in LAProof.C.cholesky]
Info.arch [definition, in LAProof.C.bandmat]
Info.arch [definition, in LAProof.C.alloc]
Info.big_endian [definition, in LAProof.C.sparse]
Info.big_endian [definition, in LAProof.C.densemat]
Info.big_endian [definition, in LAProof.C.cholesky]
Info.big_endian [definition, in LAProof.C.bandmat]
Info.big_endian [definition, in LAProof.C.alloc]
Info.bitsize [definition, in LAProof.C.sparse]
Info.bitsize [definition, in LAProof.C.densemat]
Info.bitsize [definition, in LAProof.C.cholesky]
Info.bitsize [definition, in LAProof.C.bandmat]
Info.bitsize [definition, in LAProof.C.alloc]
Info.build_branch [definition, in LAProof.C.sparse]
Info.build_tag [definition, in LAProof.C.sparse]
Info.build_number [definition, in LAProof.C.sparse]
Info.build_branch [definition, in LAProof.C.densemat]
Info.build_tag [definition, in LAProof.C.densemat]
Info.build_number [definition, in LAProof.C.densemat]
Info.build_branch [definition, in LAProof.C.cholesky]
Info.build_tag [definition, in LAProof.C.cholesky]
Info.build_number [definition, in LAProof.C.cholesky]
Info.build_branch [definition, in LAProof.C.bandmat]
Info.build_tag [definition, in LAProof.C.bandmat]
Info.build_number [definition, in LAProof.C.bandmat]
Info.build_branch [definition, in LAProof.C.alloc]
Info.build_tag [definition, in LAProof.C.alloc]
Info.build_number [definition, in LAProof.C.alloc]
Info.model [definition, in LAProof.C.sparse]
Info.model [definition, in LAProof.C.densemat]
Info.model [definition, in LAProof.C.cholesky]
Info.model [definition, in LAProof.C.bandmat]
Info.model [definition, in LAProof.C.alloc]
Info.normalized [definition, in LAProof.C.sparse]
Info.normalized [definition, in LAProof.C.densemat]
Info.normalized [definition, in LAProof.C.cholesky]
Info.normalized [definition, in LAProof.C.bandmat]
Info.normalized [definition, in LAProof.C.alloc]
Info.source_file [definition, in LAProof.C.sparse]
Info.source_file [definition, in LAProof.C.densemat]
Info.source_file [definition, in LAProof.C.cholesky]
Info.source_file [definition, in LAProof.C.bandmat]
Info.source_file [definition, in LAProof.C.alloc]
Info.version [definition, in LAProof.C.sparse]
Info.version [definition, in LAProof.C.densemat]
Info.version [definition, in LAProof.C.cholesky]
Info.version [definition, in LAProof.C.bandmat]
Info.version [definition, in LAProof.C.alloc]
int_calloc_spec [definition, in LAProof.C.spec_alloc]
in_take_ord_enum [lemma, in LAProof.C.matrix_model]
in_sublist_ord_enum [lemma, in LAProof.C.densemat_lemmas]
iota [definition, in LAProof.C.verif_cholesky]
iota_range [lemma, in LAProof.C.verif_cholesky]
iota_plus1 [lemma, in LAProof.C.verif_cholesky]
iszero [definition, in LAProof.accuracy_proofs.common]
iszeroR_iszeroF [lemma, in LAProof.accuracy_proofs.common]
is_finite_minus_no_overflow [lemma, in LAProof.accuracy_proofs.float_acc_lems]
is_finite_sum_no_overflow [lemma, in LAProof.accuracy_proofs.float_acc_lems]
is_finite_BMULT_no_overflow [lemma, in LAProof.accuracy_proofs.float_acc_lems]
is_finite_fma_no_overflow [lemma, in LAProof.accuracy_proofs.float_acc_lems]
is_finite_in [lemma, in LAProof.accuracy_proofs.sum_model]
is_finite_fma_no_overflow' [lemma, in LAProof.accuracy_proofs.fma_is_finite]
J
joinLU [definition, in LAProof.C.matrix_model]L
length_ord_enum [lemma, in LAProof.C.matrix_model]length_iota [lemma, in LAProof.C.verif_cholesky]
length_split [lemma, in LAProof.accuracy_proofs.fma_is_finite]
le_g_Sn [lemma, in LAProof.accuracy_proofs.common]
lists_of_fun [definition, in LAProof.C.verif_cholesky]
list_of_fun [definition, in LAProof.C.verif_cholesky]
lshift1 [definition, in LAProof.C.matrix_model]
M
Malloc [instance, in LAProof.C.spec_alloc]map_Rabsp_zip [lemma, in LAProof.accuracy_proofs.dotprod_model]
map_FR2_zip [lemma, in LAProof.accuracy_proofs.dotprod_model]
map_const_ord_enum [lemma, in LAProof.C.densemat_lemmas]
map2 [definition, in LAProof.C.floatlib]
matrix [definition, in LAProof.C.verif_cholesky]
matrix [definition, in LAProof.C.floatlib]
matrix_by_index_prop [lemma, in LAProof.C.floatlib]
matrix_index_prop [lemma, in LAProof.C.floatlib]
matrix_extensionality [lemma, in LAProof.C.floatlib]
matrix_extensionality_strong [lemma, in LAProof.C.floatlib]
matrix_by_index_index [lemma, in LAProof.C.floatlib]
matrix_by_index_cols [lemma, in LAProof.C.floatlib]
matrix_by_index_rows [lemma, in LAProof.C.floatlib]
matrix_cols_nat [definition, in LAProof.C.floatlib]
matrix_rows_nat [definition, in LAProof.C.floatlib]
matrix_by_index [definition, in LAProof.C.floatlib]
matrix_index [definition, in LAProof.C.floatlib]
matrix_add [definition, in LAProof.C.floatlib]
matrix_rows [definition, in LAProof.C.floatlib]
matrix_cols [definition, in LAProof.C.floatlib]
matrix_matrix_mult [definition, in LAProof.C.floatlib]
matrix_vector_mult [definition, in LAProof.C.floatlib]
matrix_model [library]
mat_axpby_error [lemma, in LAProof.accuracy_proofs.gemm_acc]
mat_sum_error [lemma, in LAProof.accuracy_proofs.gemm_acc]
mat_vec_mul_forward_error [lemma, in LAProof.accuracy_proofs.gemv_acc]
mat_vec_mul_mixed_error [lemma, in LAProof.accuracy_proofs.gemv_acc]
maxrA [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
maxrC [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
MINUS_PLUS_BOPP [lemma, in LAProof.accuracy_proofs.sum_model]
mirror_UT [definition, in LAProof.C.matrix_model]
MixedError [section, in LAProof.accuracy_proofs.dot_acc]
MixedError [section, in LAProof.accuracy_proofs.fma_dot_acc]
MixedErrorRel1 [section, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.fp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.Hfin [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.Hfp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.Hlen [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.NAN [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.t [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.v1 [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.v2 [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2 [section, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.fp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.Hfin [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.Hfp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.Hlen [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.NAN [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.t [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.v1 [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.v2 [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedError.Hfin [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.Hfin [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.Hlen [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.Hlen [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.NAN [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.NAN [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.t [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.t [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.v1 [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.v1 [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.v2 [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.v2 [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MMC_error [lemma, in LAProof.accuracy_proofs.gemm_acc]
MMERROR [section, in LAProof.accuracy_proofs.gemm_acc]
MMERROR.NAN [variable, in LAProof.accuracy_proofs.gemm_acc]
MMERROR.t [variable, in LAProof.accuracy_proofs.gemm_acc]
mult_d_e_g1_le' [lemma, in LAProof.accuracy_proofs.common]
mul_mx_row'' [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
mul_mx_row' [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
mv_mathcomp [library]
N
n [abbreviation, in LAProof.accuracy_proofs.dot_acc]n [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
N [definition, in LAProof.C.verif_cholesky]
n [abbreviation, in LAProof.accuracy_proofs.vecnorm_acc]
n [abbreviation, in LAProof.accuracy_proofs.vecnorm_acc]
NAN [section, in LAProof.accuracy_proofs.fma_is_finite]
nan_pl_1 [lemma, in LAProof.C.spec_densemat]
NAN.NAN [variable, in LAProof.accuracy_proofs.fma_is_finite]
NAN.t [variable, in LAProof.accuracy_proofs.fma_is_finite]
nan1 [definition, in LAProof.C.spec_densemat]
neg_zero [abbreviation, in LAProof.accuracy_proofs.dot_acc]
neg_zero_is_finite [lemma, in LAProof.accuracy_proofs.float_acc_lems]
neg_zero [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
neg_zero [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
neg_zero [definition, in LAProof.accuracy_proofs.common]
neg_zero [definition, in LAProof.C.matrix_model]
neg_zero [definition, in LAProof.C.verif_cholesky]
neg_zero [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
neg_zero [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
neg_zero [abbreviation, in LAProof.accuracy_proofs.sum_acc]
neg_zero [abbreviation, in LAProof.accuracy_proofs.vecnorm_acc]
neg_zero [abbreviation, in LAProof.accuracy_proofs.vecnorm_acc]
nnzF [definition, in LAProof.accuracy_proofs.common]
nnzF_is_zero_cons [lemma, in LAProof.accuracy_proofs.common]
nnzF_lemma [lemma, in LAProof.accuracy_proofs.common]
nnzF_zero [lemma, in LAProof.accuracy_proofs.common]
nnzR [abbreviation, in LAProof.accuracy_proofs.dot_acc]
nnzR [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
nnzR [definition, in LAProof.accuracy_proofs.common]
nnzR [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
nnzR [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
nnzR_cons [lemma, in LAProof.accuracy_proofs.common]
nnzR_is_zero_cons [lemma, in LAProof.accuracy_proofs.common]
nnzR_lemma [lemma, in LAProof.accuracy_proofs.common]
nnzR_zero [lemma, in LAProof.accuracy_proofs.common]
NonZeroDP [section, in LAProof.accuracy_proofs.dotprod_model]
NonZeroDP.Hlen [variable, in LAProof.accuracy_proofs.dotprod_model]
NonZeroDP.NAN [variable, in LAProof.accuracy_proofs.dotprod_model]
NonZeroDP.t [variable, in LAProof.accuracy_proofs.dotprod_model]
NonZeroDP.v1 [variable, in LAProof.accuracy_proofs.dotprod_model]
NonZeroDP.v2 [variable, in LAProof.accuracy_proofs.dotprod_model]
normM [definition, in LAProof.accuracy_proofs.mv_mathcomp]
normM_pos [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
normv [definition, in LAProof.accuracy_proofs.mv_mathcomp]
normv_triang [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
normv_pos [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
norm2 [definition, in LAProof.C.floatlib]
norm2_loose_congr [lemma, in LAProof.C.floatlib]
norm2_congr [lemma, in LAProof.C.floatlib]
norm2_snoc [lemma, in LAProof.C.floatlib]
no_overflow_minus_is_finite [lemma, in LAProof.accuracy_proofs.float_acc_lems]
no_overflow_sum_is_finite [lemma, in LAProof.accuracy_proofs.float_acc_lems]
nth_ord_enum' [lemma, in LAProof.C.matrix_model]
nth_ord_enum_lemma [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
nth_seq_of_rV [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
nth_ord_enum' [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
nth_index_enum [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
nth_List_nth [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
nth_map_inrange [lemma, in LAProof.C.floatlib]
nth_map_seq [lemma, in LAProof.C.floatlib]
nth_seq_nth [lemma, in LAProof.C.densemat_lemmas]
N_eq [definition, in LAProof.C.verif_cholesky]
O
OneNorm [section, in LAProof.accuracy_proofs.vecnorm_acc]OneNorm.Hfin [variable, in LAProof.accuracy_proofs.vecnorm_acc]
OneNorm.NAN [variable, in LAProof.accuracy_proofs.vecnorm_acc]
OneNorm.t [variable, in LAProof.accuracy_proofs.vecnorm_acc]
OneNorm.x [variable, in LAProof.accuracy_proofs.vecnorm_acc]
one_plus_d_mul_g1' [lemma, in LAProof.accuracy_proofs.common]
one_plus_d_mul_g1 [lemma, in LAProof.accuracy_proofs.common]
one_plus_d_mul_g [lemma, in LAProof.accuracy_proofs.common]
one_normR [definition, in LAProof.accuracy_proofs.vecnorm_acc]
one_normF [definition, in LAProof.accuracy_proofs.vecnorm_acc]
opp_matrix [definition, in LAProof.C.floatlib]
optfloat_to_float [definition, in LAProof.C.spec_densemat]
ordinal_enum_size [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
P
partial_row_next [lemma, in LAProof.C.sparse_model]partial_row_end [lemma, in LAProof.C.sparse_model]
partial_row_start [lemma, in LAProof.C.sparse_model]
partial_row [definition, in LAProof.C.sparse_model]
plus_e_g1_le [lemma, in LAProof.accuracy_proofs.common]
plus_d_e_g1_le [lemma, in LAProof.accuracy_proofs.common]
plus_d_e_g1_le' [lemma, in LAProof.accuracy_proofs.common]
pos_zero [definition, in LAProof.accuracy_proofs.common]
preamble [library]
pred_ord [definition, in LAProof.accuracy_proofs.mv_mathcomp]
pred_lt [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
prog [definition, in LAProof.C.sparse]
prog [definition, in LAProof.C.densemat]
prog [definition, in LAProof.C.cholesky]
prog [definition, in LAProof.C.bandmat]
prog [definition, in LAProof.C.alloc]
public_idents [definition, in LAProof.C.sparse]
public_idents [definition, in LAProof.C.densemat]
public_idents [definition, in LAProof.C.cholesky]
public_idents [definition, in LAProof.C.bandmat]
public_idents [definition, in LAProof.C.alloc]
R
Rabsp [definition, in LAProof.accuracy_proofs.dotprod_model]Rabs_sum [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
rdiv_mult_eq [lemma, in LAProof.accuracy_proofs.fma_is_finite]
rdiv_le [lemma, in LAProof.accuracy_proofs.fma_is_finite]
rdiv_lt [lemma, in LAProof.accuracy_proofs.fma_is_finite]
RealDotProd [section, in LAProof.accuracy_proofs.dotprod_model]
reptype_ftype [definition, in LAProof.C.spec_densemat]
Req_eq [lemma, in LAProof.accuracy_proofs.dotprod_model]
rev_list_rev [lemma, in LAProof.accuracy_proofs.common]
rev_ord_enum [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
Rminus_lt_minus [lemma, in LAProof.accuracy_proofs.fma_is_finite]
Rminus_le_minus [lemma, in LAProof.accuracy_proofs.fma_is_finite]
Rmult_le_lt_compat [lemma, in LAProof.accuracy_proofs.common]
rounded [definition, in LAProof.accuracy_proofs.common]
round_FT2R [lemma, in LAProof.accuracy_proofs.common]
rowmult [definition, in LAProof.C.sparse_model]
rowmult_app [lemma, in LAProof.C.sparse_model]
Rplus_le_lt_compat [lemma, in LAProof.accuracy_proofs.common]
Rplus_rewrite [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_nnzR_abs [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_nnzR [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_Rabs_eq [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_single' [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_single [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_fold_right_Rabs' [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_fold_right_Rabs [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_fold_right' [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_fold_right [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_eq [lemma, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_sind [definition, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_ind [definition, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_cons [constructor, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_nil [constructor, in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel [inductive, in LAProof.accuracy_proofs.dotprod_model]
S
scaleM_error [lemma, in LAProof.accuracy_proofs.gemm_acc]seq_of_rV [definition, in LAProof.accuracy_proofs.mv_mathcomp]
seq_rev_rev [lemma, in LAProof.C.densemat_lemmas]
size_not_empty_nat [lemma, in LAProof.accuracy_proofs.common]
size_ord_enum [lemma, in LAProof.C.matrix_model]
size_seq_of_rV [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
size_ord_enum [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
Smat_vec_mul_mixed_error [lemma, in LAProof.accuracy_proofs.vec_op_acc]
Smat_sumF_mixed_error [lemma, in LAProof.accuracy_proofs.vec_op_acc]
sMMC_error [lemma, in LAProof.accuracy_proofs.gemm_acc]
sorted_app_e1 [lemma, in LAProof.C.sparse_model]
sparse [library]
SparseASI [definition, in LAProof.C.spec_sparse]
SparseErrorRel1 [section, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.fp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.Hfin [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.Hfp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.Hlen [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.Hra [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.Hrp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.NAN [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.rp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.rp_abs [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.t [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.v1 [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.v2 [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2 [section, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.fp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.Hfin [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.Hfp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.Hlen [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.Hra [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.Hrp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.NAN [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.rp [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.rp_abs [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.t [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.v1 [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.v2 [variable, in LAProof.accuracy_proofs.dot_acc_lemmas]
sparseImports [definition, in LAProof.C.VSU_sparse]
SparseVSU [definition, in LAProof.C.VSU_sparse]
sparse_dotprod_forward_error [lemma, in LAProof.accuracy_proofs.dot_acc]
sparse_fma_dotprod_forward_error [lemma, in LAProof.accuracy_proofs.dot_acc_lemmas]
sparse_dotprod_forward_error_rel [lemma, in LAProof.accuracy_proofs.dot_acc_lemmas]
sparse_model [library]
spec_densemat [library]
spec_alloc [library]
spec_sparse [library]
strict_floatlist_eqv_i [lemma, in LAProof.C.sparse_model]
strict_feq_i [lemma, in LAProof.C.sparse_model]
subMultNorm [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
SubsetMathASI [definition, in LAProof.C.spec_sparse]
subtractoff_spec [definition, in LAProof.C.spec_densemat]
subtract_another [lemma, in LAProof.C.matrix_model]
subtract_loop' [definition, in LAProof.C.matrix_model]
subtract_loop [definition, in LAProof.C.matrix_model]
subtract_loop_sum_any [lemma, in LAProof.accuracy_proofs.sum_model]
subtract_loop_sumR [lemma, in LAProof.accuracy_proofs.sum_model]
subtract_loop_congr1 [lemma, in LAProof.accuracy_proofs.sum_model]
subtract_loop [definition, in LAProof.accuracy_proofs.sum_model]
subtract_another [lemma, in LAProof.C.verif_cholesky]
subtract_loop [definition, in LAProof.C.verif_cholesky]
sumF [definition, in LAProof.accuracy_proofs.sum_model]
sumF [definition, in LAProof.C.verif_cholesky]
sumR [definition, in LAProof.accuracy_proofs.sum_model]
sumRabs_Rabs [lemma, in LAProof.accuracy_proofs.sum_model]
sumRabs_pos [lemma, in LAProof.accuracy_proofs.sum_model]
sumR_sum [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
sumR_rev [lemma, in LAProof.accuracy_proofs.sum_model]
sumR_permute [lemma, in LAProof.accuracy_proofs.sum_model]
sumR_app_cons [lemma, in LAProof.accuracy_proofs.sum_model]
sumR_le_sumRabs [lemma, in LAProof.accuracy_proofs.sum_model]
sumR_mult [lemma, in LAProof.accuracy_proofs.sum_model]
sum_any_sind [definition, in LAProof.C.matrix_model]
sum_any_ind [definition, in LAProof.C.matrix_model]
Sum_Any_perm [constructor, in LAProof.C.matrix_model]
Sum_Any_split [constructor, in LAProof.C.matrix_model]
Sum_Any_1 [constructor, in LAProof.C.matrix_model]
Sum_Any_0 [constructor, in LAProof.C.matrix_model]
sum_any [inductive, in LAProof.C.matrix_model]
sum_abs [definition, in LAProof.accuracy_proofs.mv_mathcomp]
sum_rel_Ft_exists [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_Ft_fold [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_abs_exists [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_exists [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_Ft_single [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_Ft [definition, in LAProof.accuracy_proofs.sum_model]
sum_map_Rmult [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_fold [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_bound'' [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_bound' [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_permute_t [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_permute [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_bound [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_app_cons [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_single' [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_single [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_Rabs [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_Rabs_eq [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_Rabs_pos [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_R_abs [lemma, in LAProof.accuracy_proofs.sum_model]
sum_rel_sum_any [lemma, in LAProof.accuracy_proofs.sum_model]
sum_any_sind [definition, in LAProof.accuracy_proofs.sum_model]
sum_any_ind [definition, in LAProof.accuracy_proofs.sum_model]
Sum_Any_Some [constructor, in LAProof.accuracy_proofs.sum_model]
Sum_Any_None [constructor, in LAProof.accuracy_proofs.sum_model]
sum_any [inductive, in LAProof.accuracy_proofs.sum_model]
sum_any'_sind [definition, in LAProof.accuracy_proofs.sum_model]
sum_any'_ind [definition, in LAProof.accuracy_proofs.sum_model]
Sum_Any_perm [constructor, in LAProof.accuracy_proofs.sum_model]
Sum_Any_split [constructor, in LAProof.accuracy_proofs.sum_model]
Sum_Any_1 [constructor, in LAProof.accuracy_proofs.sum_model]
sum_any' [inductive, in LAProof.accuracy_proofs.sum_model]
sum_rel_R [definition, in LAProof.accuracy_proofs.sum_model]
sum_rel_sind [definition, in LAProof.accuracy_proofs.sum_model]
sum_rel_ind [definition, in LAProof.accuracy_proofs.sum_model]
sum_rel_cons [constructor, in LAProof.accuracy_proofs.sum_model]
sum_rel_nil [constructor, in LAProof.accuracy_proofs.sum_model]
sum_rel [inductive, in LAProof.accuracy_proofs.sum_model]
sum_upto [definition, in LAProof.C.verif_cholesky]
sum_rel_R_abs_exists_fma [lemma, in LAProof.accuracy_proofs.dotprod_model]
sum_rev [lemma, in LAProof.accuracy_proofs.dotprod_model]
sum_fold [definition, in LAProof.accuracy_proofs.dotprod_model]
sum_forward_error_permute [lemma, in LAProof.accuracy_proofs.sum_acc]
sum_forward_error_permute' [lemma, in LAProof.accuracy_proofs.sum_acc]
sum_model [library]
sum_acc [library]
surely_malloc_spec_sub [lemma, in LAProof.C.spec_alloc]
surely_malloc_spec [definition, in LAProof.C.spec_alloc]
surely_malloc_spec' [definition, in LAProof.C.spec_alloc]
T
take_snoc [lemma, in LAProof.C.matrix_model]take_sublist [lemma, in LAProof.C.densemat_lemmas]
the_loop_body [definition, in LAProof.C.verif_sparse]
the_type [definition, in LAProof.C.spec_densemat]
the_ctype [definition, in LAProof.C.spec_densemat]
TwoNorm [section, in LAProof.accuracy_proofs.vecnorm_acc]
TwoNorm.Hfin [variable, in LAProof.accuracy_proofs.vecnorm_acc]
TwoNorm.NAN [variable, in LAProof.accuracy_proofs.vecnorm_acc]
TwoNorm.t [variable, in LAProof.accuracy_proofs.vecnorm_acc]
TwoNorm.x [variable, in LAProof.accuracy_proofs.vecnorm_acc]
two_normR [definition, in LAProof.accuracy_proofs.vecnorm_acc]
two_normF [definition, in LAProof.accuracy_proofs.vecnorm_acc]
t_crs [definition, in LAProof.C.spec_sparse]
U
update_i_lt_j [lemma, in LAProof.C.matrix_model]update_i_lt_j_aux [lemma, in LAProof.C.matrix_model]
update_mx [definition, in LAProof.C.matrix_model]
update_i_lt_j [lemma, in LAProof.C.verif_cholesky]
updij [definition, in LAProof.C.verif_cholesky]
upd_Znth_lists_of_fun [lemma, in LAProof.C.verif_cholesky]
upd_Znth_column_major [lemma, in LAProof.C.densemat_lemmas]
upto_row_col [definition, in LAProof.C.verif_densemat_mult]
upto_iota [lemma, in LAProof.C.verif_cholesky]
V
val_of_optfloat [definition, in LAProof.C.spec_densemat]val_of_float [definition, in LAProof.C.spec_densemat]
val_of_optfloat_column_major [lemma, in LAProof.C.densemat_lemmas]
vecnorm_acc [library]
vector [definition, in LAProof.C.floatlib]
vector_sub_congr [lemma, in LAProof.C.floatlib]
vector_sub [definition, in LAProof.C.floatlib]
vector_add [definition, in LAProof.C.floatlib]
vec_vec_mul_mixed_error [lemma, in LAProof.accuracy_proofs.gemv_acc]
vec_op_acc [library]
verif_densemat [library]
verif_alloc [library]
verif_cholesky [library]
verif_densemat_cholesky [library]
verif_densemat_mult [library]
verif_sparse [library]
verif_sparse_byrows [library]
vF [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
vF [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
Vprog [definition, in LAProof.C.spec_densemat]
Vprog [definition, in LAProof.C.spec_alloc]
Vprog [definition, in LAProof.C.verif_cholesky]
Vprog [definition, in LAProof.C.spec_sparse]
vR [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
vR [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
vR' [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
vR' [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
VSU_densemat [library]
VSU_sparse [library]
v___stringlit_2 [definition, in LAProof.C.densemat]
v___stringlit_5 [definition, in LAProof.C.densemat]
v___stringlit_3 [definition, in LAProof.C.densemat]
v___stringlit_7 [definition, in LAProof.C.densemat]
v___stringlit_6 [definition, in LAProof.C.densemat]
v___stringlit_4 [definition, in LAProof.C.densemat]
v___stringlit_1 [definition, in LAProof.C.densemat]
v___stringlit_4 [definition, in LAProof.C.bandmat]
v___stringlit_2 [definition, in LAProof.C.bandmat]
v___stringlit_5 [definition, in LAProof.C.bandmat]
v___stringlit_1 [definition, in LAProof.C.bandmat]
v___stringlit_3 [definition, in LAProof.C.bandmat]
v1R [abbreviation, in LAProof.accuracy_proofs.dot_acc]
v1R [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
v1R [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
v1R [abbreviation, in LAProof.accuracy_proofs.dot_acc_lemmas]
v1R [abbreviation, in LAProof.accuracy_proofs.dotprod_model]
v1R' [abbreviation, in LAProof.accuracy_proofs.dot_acc]
v1R' [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
v2R [abbreviation, in LAProof.accuracy_proofs.dot_acc]
v2R [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
v2R' [abbreviation, in LAProof.accuracy_proofs.dot_acc]
v2R' [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
W
WithNan [section, in LAProof.accuracy_proofs.sum_acc]WithNAN [section, in LAProof.accuracy_proofs.gemv_acc]
WithNans [section, in LAProof.accuracy_proofs.vec_op_acc]
WithNans.NAN [variable, in LAProof.accuracy_proofs.vec_op_acc]
WithNans.t [variable, in LAProof.accuracy_proofs.vec_op_acc]
WithNan.NAN [variable, in LAProof.accuracy_proofs.sum_acc]
WithNAN.NAN [variable, in LAProof.accuracy_proofs.gemv_acc]
WithNan.t [variable, in LAProof.accuracy_proofs.sum_acc]
WithNAN.t [variable, in LAProof.accuracy_proofs.gemv_acc]
WithSTD [section, in LAProof.accuracy_proofs.sum_model]
WithSTD [section, in LAProof.C.verif_cholesky]
WithSTD.NAN [variable, in LAProof.accuracy_proofs.sum_model]
WithSTD.NAN [variable, in LAProof.C.verif_cholesky]
WithSTD.STD [variable, in LAProof.C.verif_cholesky]
WithSTD.t [variable, in LAProof.accuracy_proofs.sum_model]
WithSTD.t [variable, in LAProof.C.verif_cholesky]
WithType [section, in LAProof.accuracy_proofs.common]
WithType [section, in LAProof.accuracy_proofs.common]
WithType.NAN [variable, in LAProof.accuracy_proofs.common]
WithType.NAN [variable, in LAProof.accuracy_proofs.common]
WithType.t [variable, in LAProof.accuracy_proofs.common]
WithType.t [variable, in LAProof.accuracy_proofs.common]
X
xR [abbreviation, in LAProof.accuracy_proofs.vecnorm_acc]xR [abbreviation, in LAProof.accuracy_proofs.vecnorm_acc]
Z
zerof [instance, in LAProof.C.matrix_model]zerof [instance, in LAProof.C.floatlib]
Zlength_iota [lemma, in LAProof.C.verif_cholesky]
Zlength_seq [lemma, in LAProof.C.floatlib]
Zlength_column_major [lemma, in LAProof.C.densemat_lemmas]
Zlength_ord_enum [lemma, in LAProof.C.densemat_lemmas]
Zmatrix_rows_nat [lemma, in LAProof.C.floatlib]
Zmatrix_cols_nat [lemma, in LAProof.C.floatlib]
Znth_lists_done [lemma, in LAProof.C.verif_cholesky]
Znth_i_list_of_fun [lemma, in LAProof.C.verif_cholesky]
Znth_i_iota [lemma, in LAProof.C.verif_cholesky]
Znth_vector_sub [lemma, in LAProof.C.floatlib]
Znth_column_major [lemma, in LAProof.C.densemat_lemmas]
Znth_ord_enum [lemma, in LAProof.C.densemat_lemmas]
_
_t'2 [definition, in LAProof.C.sparse]_t'1 [definition, in LAProof.C.sparse]
_y [definition, in LAProof.C.sparse]
_x [definition, in LAProof.C.sparse]
_val [definition, in LAProof.C.sparse]
_v [definition, in LAProof.C.sparse]
_s [definition, in LAProof.C.sparse]
_rows [definition, in LAProof.C.sparse]
_row_ptr [definition, in LAProof.C.sparse]
_p [definition, in LAProof.C.sparse]
_next [definition, in LAProof.C.sparse]
_main [definition, in LAProof.C.sparse]
_m [definition, in LAProof.C.sparse]
_j [definition, in LAProof.C.sparse]
_i [definition, in LAProof.C.sparse]
_hi [definition, in LAProof.C.sparse]
_h [definition, in LAProof.C.sparse]
_fma [definition, in LAProof.C.sparse]
_crs_row_vector_multiply [definition, in LAProof.C.sparse]
_crs_matrix_vector_multiply_byrows [definition, in LAProof.C.sparse]
_crs_matrix_vector_multiply [definition, in LAProof.C.sparse]
_crs_matrix_rows [definition, in LAProof.C.sparse]
_crs_matrix [definition, in LAProof.C.sparse]
_cols [definition, in LAProof.C.sparse]
_col_ind [definition, in LAProof.C.sparse]
___compcert_va_int64 [definition, in LAProof.C.sparse]
___compcert_va_int32 [definition, in LAProof.C.sparse]
___compcert_va_float64 [definition, in LAProof.C.sparse]
___compcert_va_composite [definition, in LAProof.C.sparse]
___compcert_i64_utof [definition, in LAProof.C.sparse]
___compcert_i64_utod [definition, in LAProof.C.sparse]
___compcert_i64_umulh [definition, in LAProof.C.sparse]
___compcert_i64_umod [definition, in LAProof.C.sparse]
___compcert_i64_udiv [definition, in LAProof.C.sparse]
___compcert_i64_stof [definition, in LAProof.C.sparse]
___compcert_i64_stod [definition, in LAProof.C.sparse]
___compcert_i64_smulh [definition, in LAProof.C.sparse]
___compcert_i64_smod [definition, in LAProof.C.sparse]
___compcert_i64_shr [definition, in LAProof.C.sparse]
___compcert_i64_shl [definition, in LAProof.C.sparse]
___compcert_i64_sdiv [definition, in LAProof.C.sparse]
___compcert_i64_sar [definition, in LAProof.C.sparse]
___compcert_i64_dtou [definition, in LAProof.C.sparse]
___compcert_i64_dtos [definition, in LAProof.C.sparse]
___builtin_va_start [definition, in LAProof.C.sparse]
___builtin_va_end [definition, in LAProof.C.sparse]
___builtin_va_copy [definition, in LAProof.C.sparse]
___builtin_va_arg [definition, in LAProof.C.sparse]
___builtin_unreachable [definition, in LAProof.C.sparse]
___builtin_sqrt [definition, in LAProof.C.sparse]
___builtin_sel [definition, in LAProof.C.sparse]
___builtin_memcpy_aligned [definition, in LAProof.C.sparse]
___builtin_membar [definition, in LAProof.C.sparse]
___builtin_fsqrt [definition, in LAProof.C.sparse]
___builtin_fnmsub [definition, in LAProof.C.sparse]
___builtin_fnmadd [definition, in LAProof.C.sparse]
___builtin_fmsub [definition, in LAProof.C.sparse]
___builtin_fmin [definition, in LAProof.C.sparse]
___builtin_fmax [definition, in LAProof.C.sparse]
___builtin_fmadd [definition, in LAProof.C.sparse]
___builtin_fabsf [definition, in LAProof.C.sparse]
___builtin_fabs [definition, in LAProof.C.sparse]
___builtin_expect [definition, in LAProof.C.sparse]
___builtin_debug [definition, in LAProof.C.sparse]
___builtin_ctzll [definition, in LAProof.C.sparse]
___builtin_ctzl [definition, in LAProof.C.sparse]
___builtin_ctz [definition, in LAProof.C.sparse]
___builtin_clzll [definition, in LAProof.C.sparse]
___builtin_clzl [definition, in LAProof.C.sparse]
___builtin_clz [definition, in LAProof.C.sparse]
___builtin_clsll [definition, in LAProof.C.sparse]
___builtin_clsl [definition, in LAProof.C.sparse]
___builtin_cls [definition, in LAProof.C.sparse]
___builtin_bswap64 [definition, in LAProof.C.sparse]
___builtin_bswap32 [definition, in LAProof.C.sparse]
___builtin_bswap16 [definition, in LAProof.C.sparse]
___builtin_bswap [definition, in LAProof.C.sparse]
___builtin_annot_intval [definition, in LAProof.C.sparse]
___builtin_annot [definition, in LAProof.C.sparse]
_t'9 [definition, in LAProof.C.densemat]
_t'8 [definition, in LAProof.C.densemat]
_t'7 [definition, in LAProof.C.densemat]
_t'6 [definition, in LAProof.C.densemat]
_t'5 [definition, in LAProof.C.densemat]
_t'4 [definition, in LAProof.C.densemat]
_t'3 [definition, in LAProof.C.densemat]
_t'2 [definition, in LAProof.C.densemat]
_t'10 [definition, in LAProof.C.densemat]
_t'1 [definition, in LAProof.C.densemat]
_z [definition, in LAProof.C.densemat]
_yi [definition, in LAProof.C.densemat]
_y [definition, in LAProof.C.densemat]
_xj [definition, in LAProof.C.densemat]
_x [definition, in LAProof.C.densemat]
_vm [definition, in LAProof.C.densemat]
_t [definition, in LAProof.C.densemat]
_surely_malloc [definition, in LAProof.C.densemat]
_subtractoff [definition, in LAProof.C.densemat]
_sqrt [definition, in LAProof.C.densemat]
_s [definition, in LAProof.C.densemat]
_rows [definition, in LAProof.C.densemat]
_rkk [definition, in LAProof.C.densemat]
_rkj [definition, in LAProof.C.densemat]
_result [definition, in LAProof.C.densemat]
_printf [definition, in LAProof.C.densemat]
_p [definition, in LAProof.C.densemat]
_nswap [definition, in LAProof.C.densemat]
_n [definition, in LAProof.C.densemat]
_main [definition, in LAProof.C.densemat]
_m [definition, in LAProof.C.densemat]
_l [definition, in LAProof.C.densemat]
_k__1 [definition, in LAProof.C.densemat]
_k [definition, in LAProof.C.densemat]
_j__1 [definition, in LAProof.C.densemat]
_j [definition, in LAProof.C.densemat]
_ipivj [definition, in LAProof.C.densemat]
_ipiv [definition, in LAProof.C.densemat]
_i__2 [definition, in LAProof.C.densemat]
_i__1 [definition, in LAProof.C.densemat]
_i [definition, in LAProof.C.densemat]
_h [definition, in LAProof.C.densemat]
_free [definition, in LAProof.C.densemat]
_fma [definition, in LAProof.C.densemat]
_fabs [definition, in LAProof.C.densemat]
_double_clear [definition, in LAProof.C.densemat]
_dm [definition, in LAProof.C.densemat]
_densematn_set [definition, in LAProof.C.densemat]
_densematn_print [definition, in LAProof.C.densemat]
_densematn_mult [definition, in LAProof.C.densemat]
_densematn_lusolveT [definition, in LAProof.C.densemat]
_densematn_lusolve [definition, in LAProof.C.densemat]
_densematn_lujac [definition, in LAProof.C.densemat]
_densematn_lufactor [definition, in LAProof.C.densemat]
_densematn_get [definition, in LAProof.C.densemat]
_densematn_dotprod [definition, in LAProof.C.densemat]
_densematn_csolve [definition, in LAProof.C.densemat]
_densematn_clear [definition, in LAProof.C.densemat]
_densematn_cfactor_outer [definition, in LAProof.C.densemat]
_densematn_cfactor_block [definition, in LAProof.C.densemat]
_densematn_cfactor [definition, in LAProof.C.densemat]
_densematn_addto [definition, in LAProof.C.densemat]
_densemat_t [definition, in LAProof.C.densemat]
_densemat_set [definition, in LAProof.C.densemat]
_densemat_print [definition, in LAProof.C.densemat]
_densemat_norm2 [definition, in LAProof.C.densemat]
_densemat_norm [definition, in LAProof.C.densemat]
_densemat_mult [definition, in LAProof.C.densemat]
_densemat_malloc [definition, in LAProof.C.densemat]
_densemat_lusolveT [definition, in LAProof.C.densemat]
_densemat_lusolve [definition, in LAProof.C.densemat]
_densemat_lujac [definition, in LAProof.C.densemat]
_densemat_lufactor [definition, in LAProof.C.densemat]
_densemat_get [definition, in LAProof.C.densemat]
_densemat_free [definition, in LAProof.C.densemat]
_densemat_dotprod [definition, in LAProof.C.densemat]
_densemat_csolve [definition, in LAProof.C.densemat]
_densemat_clear [definition, in LAProof.C.densemat]
_densemat_cfactor [definition, in LAProof.C.densemat]
_densemat_addto [definition, in LAProof.C.densemat]
_data_norm2 [definition, in LAProof.C.densemat]
_data_norm [definition, in LAProof.C.densemat]
_data [definition, in LAProof.C.densemat]
_c [definition, in LAProof.C.densemat]
_blocksolve [definition, in LAProof.C.densemat]
_bi [definition, in LAProof.C.densemat]
_b [definition, in LAProof.C.densemat]
_akk [definition, in LAProof.C.densemat]
_abort [definition, in LAProof.C.densemat]
___stringlit_7 [definition, in LAProof.C.densemat]
___stringlit_6 [definition, in LAProof.C.densemat]
___stringlit_5 [definition, in LAProof.C.densemat]
___stringlit_4 [definition, in LAProof.C.densemat]
___stringlit_3 [definition, in LAProof.C.densemat]
___stringlit_2 [definition, in LAProof.C.densemat]
___stringlit_1 [definition, in LAProof.C.densemat]
___compcert_va_int64 [definition, in LAProof.C.densemat]
___compcert_va_int32 [definition, in LAProof.C.densemat]
___compcert_va_float64 [definition, in LAProof.C.densemat]
___compcert_va_composite [definition, in LAProof.C.densemat]
___compcert_i64_utof [definition, in LAProof.C.densemat]
___compcert_i64_utod [definition, in LAProof.C.densemat]
___compcert_i64_umulh [definition, in LAProof.C.densemat]
___compcert_i64_umod [definition, in LAProof.C.densemat]
___compcert_i64_udiv [definition, in LAProof.C.densemat]
___compcert_i64_stof [definition, in LAProof.C.densemat]
___compcert_i64_stod [definition, in LAProof.C.densemat]
___compcert_i64_smulh [definition, in LAProof.C.densemat]
___compcert_i64_smod [definition, in LAProof.C.densemat]
___compcert_i64_shr [definition, in LAProof.C.densemat]
___compcert_i64_shl [definition, in LAProof.C.densemat]
___compcert_i64_sdiv [definition, in LAProof.C.densemat]
___compcert_i64_sar [definition, in LAProof.C.densemat]
___compcert_i64_dtou [definition, in LAProof.C.densemat]
___compcert_i64_dtos [definition, in LAProof.C.densemat]
___builtin_va_start [definition, in LAProof.C.densemat]
___builtin_va_end [definition, in LAProof.C.densemat]
___builtin_va_copy [definition, in LAProof.C.densemat]
___builtin_va_arg [definition, in LAProof.C.densemat]
___builtin_unreachable [definition, in LAProof.C.densemat]
___builtin_sqrt [definition, in LAProof.C.densemat]
___builtin_sel [definition, in LAProof.C.densemat]
___builtin_memcpy_aligned [definition, in LAProof.C.densemat]
___builtin_membar [definition, in LAProof.C.densemat]
___builtin_fsqrt [definition, in LAProof.C.densemat]
___builtin_fnmsub [definition, in LAProof.C.densemat]
___builtin_fnmadd [definition, in LAProof.C.densemat]
___builtin_fmsub [definition, in LAProof.C.densemat]
___builtin_fmin [definition, in LAProof.C.densemat]
___builtin_fmax [definition, in LAProof.C.densemat]
___builtin_fmadd [definition, in LAProof.C.densemat]
___builtin_fabsf [definition, in LAProof.C.densemat]
___builtin_fabs [definition, in LAProof.C.densemat]
___builtin_expect [definition, in LAProof.C.densemat]
___builtin_debug [definition, in LAProof.C.densemat]
___builtin_ctzll [definition, in LAProof.C.densemat]
___builtin_ctzl [definition, in LAProof.C.densemat]
___builtin_ctz [definition, in LAProof.C.densemat]
___builtin_clzll [definition, in LAProof.C.densemat]
___builtin_clzl [definition, in LAProof.C.densemat]
___builtin_clz [definition, in LAProof.C.densemat]
___builtin_clsll [definition, in LAProof.C.densemat]
___builtin_clsl [definition, in LAProof.C.densemat]
___builtin_cls [definition, in LAProof.C.densemat]
___builtin_bswap64 [definition, in LAProof.C.densemat]
___builtin_bswap32 [definition, in LAProof.C.densemat]
___builtin_bswap16 [definition, in LAProof.C.densemat]
___builtin_bswap [definition, in LAProof.C.densemat]
___builtin_annot_intval [definition, in LAProof.C.densemat]
___builtin_annot [definition, in LAProof.C.densemat]
_Ujk [definition, in LAProof.C.densemat]
_Ujj [definition, in LAProof.C.densemat]
_R [definition, in LAProof.C.densemat]
_Lij [definition, in LAProof.C.densemat]
_J [definition, in LAProof.C.densemat]
_A [definition, in LAProof.C.densemat]
_t'4 [definition, in LAProof.C.cholesky]
_t'3 [definition, in LAProof.C.cholesky]
_t'2 [definition, in LAProof.C.cholesky]
_t'1 [definition, in LAProof.C.cholesky]
_sqrt [definition, in LAProof.C.cholesky]
_s [definition, in LAProof.C.cholesky]
_rkj [definition, in LAProof.C.cholesky]
_n [definition, in LAProof.C.cholesky]
_main [definition, in LAProof.C.cholesky]
_k [definition, in LAProof.C.cholesky]
_j [definition, in LAProof.C.cholesky]
_i [definition, in LAProof.C.cholesky]
_cholesky [definition, in LAProof.C.cholesky]
___compcert_va_int64 [definition, in LAProof.C.cholesky]
___compcert_va_int32 [definition, in LAProof.C.cholesky]
___compcert_va_float64 [definition, in LAProof.C.cholesky]
___compcert_va_composite [definition, in LAProof.C.cholesky]
___compcert_i64_utof [definition, in LAProof.C.cholesky]
___compcert_i64_utod [definition, in LAProof.C.cholesky]
___compcert_i64_umulh [definition, in LAProof.C.cholesky]
___compcert_i64_umod [definition, in LAProof.C.cholesky]
___compcert_i64_udiv [definition, in LAProof.C.cholesky]
___compcert_i64_stof [definition, in LAProof.C.cholesky]
___compcert_i64_stod [definition, in LAProof.C.cholesky]
___compcert_i64_smulh [definition, in LAProof.C.cholesky]
___compcert_i64_smod [definition, in LAProof.C.cholesky]
___compcert_i64_shr [definition, in LAProof.C.cholesky]
___compcert_i64_shl [definition, in LAProof.C.cholesky]
___compcert_i64_sdiv [definition, in LAProof.C.cholesky]
___compcert_i64_sar [definition, in LAProof.C.cholesky]
___compcert_i64_dtou [definition, in LAProof.C.cholesky]
___compcert_i64_dtos [definition, in LAProof.C.cholesky]
___builtin_va_start [definition, in LAProof.C.cholesky]
___builtin_va_end [definition, in LAProof.C.cholesky]
___builtin_va_copy [definition, in LAProof.C.cholesky]
___builtin_va_arg [definition, in LAProof.C.cholesky]
___builtin_unreachable [definition, in LAProof.C.cholesky]
___builtin_sqrt [definition, in LAProof.C.cholesky]
___builtin_sel [definition, in LAProof.C.cholesky]
___builtin_memcpy_aligned [definition, in LAProof.C.cholesky]
___builtin_membar [definition, in LAProof.C.cholesky]
___builtin_fsqrt [definition, in LAProof.C.cholesky]
___builtin_fnmsub [definition, in LAProof.C.cholesky]
___builtin_fnmadd [definition, in LAProof.C.cholesky]
___builtin_fmsub [definition, in LAProof.C.cholesky]
___builtin_fmin [definition, in LAProof.C.cholesky]
___builtin_fmax [definition, in LAProof.C.cholesky]
___builtin_fmadd [definition, in LAProof.C.cholesky]
___builtin_fabsf [definition, in LAProof.C.cholesky]
___builtin_fabs [definition, in LAProof.C.cholesky]
___builtin_expect [definition, in LAProof.C.cholesky]
___builtin_debug [definition, in LAProof.C.cholesky]
___builtin_ctzll [definition, in LAProof.C.cholesky]
___builtin_ctzl [definition, in LAProof.C.cholesky]
___builtin_ctz [definition, in LAProof.C.cholesky]
___builtin_clzll [definition, in LAProof.C.cholesky]
___builtin_clzl [definition, in LAProof.C.cholesky]
___builtin_clz [definition, in LAProof.C.cholesky]
___builtin_clsll [definition, in LAProof.C.cholesky]
___builtin_clsl [definition, in LAProof.C.cholesky]
___builtin_cls [definition, in LAProof.C.cholesky]
___builtin_bswap64 [definition, in LAProof.C.cholesky]
___builtin_bswap32 [definition, in LAProof.C.cholesky]
___builtin_bswap16 [definition, in LAProof.C.cholesky]
___builtin_bswap [definition, in LAProof.C.cholesky]
___builtin_annot_intval [definition, in LAProof.C.cholesky]
___builtin_annot [definition, in LAProof.C.cholesky]
_R [definition, in LAProof.C.cholesky]
_A [definition, in LAProof.C.cholesky]
_t'9 [definition, in LAProof.C.bandmat]
_t'8 [definition, in LAProof.C.bandmat]
_t'7 [definition, in LAProof.C.bandmat]
_t'6 [definition, in LAProof.C.bandmat]
_t'5 [definition, in LAProof.C.bandmat]
_t'4 [definition, in LAProof.C.bandmat]
_t'3 [definition, in LAProof.C.bandmat]
_t'2 [definition, in LAProof.C.bandmat]
_t'1 [definition, in LAProof.C.bandmat]
_yi [definition, in LAProof.C.bandmat]
_x [definition, in LAProof.C.bandmat]
_vm [definition, in LAProof.C.bandmat]
_surely_malloc [definition, in LAProof.C.bandmat]
_sqrt [definition, in LAProof.C.bandmat]
_rows [definition, in LAProof.C.bandmat]
_printf [definition, in LAProof.C.bandmat]
_n [definition, in LAProof.C.bandmat]
_memset [definition, in LAProof.C.bandmat]
_main [definition, in LAProof.C.bandmat]
_m [definition, in LAProof.C.bandmat]
_k [definition, in LAProof.C.bandmat]
_j__1 [definition, in LAProof.C.bandmat]
_j [definition, in LAProof.C.bandmat]
_i__1 [definition, in LAProof.C.bandmat]
_i [definition, in LAProof.C.bandmat]
_free [definition, in LAProof.C.bandmat]
_dm [definition, in LAProof.C.bandmat]
_dj [definition, in LAProof.C.bandmat]
_densemat_t [definition, in LAProof.C.bandmat]
_densemat_get [definition, in LAProof.C.bandmat]
_dense_to_band [definition, in LAProof.C.bandmat]
_data_norm2 [definition, in LAProof.C.bandmat]
_data_norm [definition, in LAProof.C.bandmat]
_data [definition, in LAProof.C.bandmat]
_d [definition, in LAProof.C.bandmat]
_bw [definition, in LAProof.C.bandmat]
_bi [definition, in LAProof.C.bandmat]
_bandmatn_set [definition, in LAProof.C.bandmat]
_bandmatn_get [definition, in LAProof.C.bandmat]
_bandmatn_clear [definition, in LAProof.C.bandmat]
_bandmatn_addto [definition, in LAProof.C.bandmat]
_bandmat_t [definition, in LAProof.C.bandmat]
_bandmat_solve [definition, in LAProof.C.bandmat]
_bandmat_set [definition, in LAProof.C.bandmat]
_bandmat_print [definition, in LAProof.C.bandmat]
_bandmat_norm2 [definition, in LAProof.C.bandmat]
_bandmat_norm [definition, in LAProof.C.bandmat]
_bandmat_malloc [definition, in LAProof.C.bandmat]
_bandmat_get [definition, in LAProof.C.bandmat]
_bandmat_free [definition, in LAProof.C.bandmat]
_bandmat_factor [definition, in LAProof.C.bandmat]
_bandmat_clear [definition, in LAProof.C.bandmat]
_bandmat_addto [definition, in LAProof.C.bandmat]
_b [definition, in LAProof.C.bandmat]
_abort [definition, in LAProof.C.bandmat]
___stringlit_5 [definition, in LAProof.C.bandmat]
___stringlit_4 [definition, in LAProof.C.bandmat]
___stringlit_3 [definition, in LAProof.C.bandmat]
___stringlit_2 [definition, in LAProof.C.bandmat]
___stringlit_1 [definition, in LAProof.C.bandmat]
___compcert_va_int64 [definition, in LAProof.C.bandmat]
___compcert_va_int32 [definition, in LAProof.C.bandmat]
___compcert_va_float64 [definition, in LAProof.C.bandmat]
___compcert_va_composite [definition, in LAProof.C.bandmat]
___compcert_i64_utof [definition, in LAProof.C.bandmat]
___compcert_i64_utod [definition, in LAProof.C.bandmat]
___compcert_i64_umulh [definition, in LAProof.C.bandmat]
___compcert_i64_umod [definition, in LAProof.C.bandmat]
___compcert_i64_udiv [definition, in LAProof.C.bandmat]
___compcert_i64_stof [definition, in LAProof.C.bandmat]
___compcert_i64_stod [definition, in LAProof.C.bandmat]
___compcert_i64_smulh [definition, in LAProof.C.bandmat]
___compcert_i64_smod [definition, in LAProof.C.bandmat]
___compcert_i64_shr [definition, in LAProof.C.bandmat]
___compcert_i64_shl [definition, in LAProof.C.bandmat]
___compcert_i64_sdiv [definition, in LAProof.C.bandmat]
___compcert_i64_sar [definition, in LAProof.C.bandmat]
___compcert_i64_dtou [definition, in LAProof.C.bandmat]
___compcert_i64_dtos [definition, in LAProof.C.bandmat]
___builtin_va_start [definition, in LAProof.C.bandmat]
___builtin_va_end [definition, in LAProof.C.bandmat]
___builtin_va_copy [definition, in LAProof.C.bandmat]
___builtin_va_arg [definition, in LAProof.C.bandmat]
___builtin_unreachable [definition, in LAProof.C.bandmat]
___builtin_sqrt [definition, in LAProof.C.bandmat]
___builtin_sel [definition, in LAProof.C.bandmat]
___builtin_memcpy_aligned [definition, in LAProof.C.bandmat]
___builtin_membar [definition, in LAProof.C.bandmat]
___builtin_fsqrt [definition, in LAProof.C.bandmat]
___builtin_fnmsub [definition, in LAProof.C.bandmat]
___builtin_fnmadd [definition, in LAProof.C.bandmat]
___builtin_fmsub [definition, in LAProof.C.bandmat]
___builtin_fmin [definition, in LAProof.C.bandmat]
___builtin_fmax [definition, in LAProof.C.bandmat]
___builtin_fmadd [definition, in LAProof.C.bandmat]
___builtin_fabsf [definition, in LAProof.C.bandmat]
___builtin_fabs [definition, in LAProof.C.bandmat]
___builtin_expect [definition, in LAProof.C.bandmat]
___builtin_debug [definition, in LAProof.C.bandmat]
___builtin_ctzll [definition, in LAProof.C.bandmat]
___builtin_ctzl [definition, in LAProof.C.bandmat]
___builtin_ctz [definition, in LAProof.C.bandmat]
___builtin_clzll [definition, in LAProof.C.bandmat]
___builtin_clzl [definition, in LAProof.C.bandmat]
___builtin_clz [definition, in LAProof.C.bandmat]
___builtin_clsll [definition, in LAProof.C.bandmat]
___builtin_clsl [definition, in LAProof.C.bandmat]
___builtin_cls [definition, in LAProof.C.bandmat]
___builtin_bswap64 [definition, in LAProof.C.bandmat]
___builtin_bswap32 [definition, in LAProof.C.bandmat]
___builtin_bswap16 [definition, in LAProof.C.bandmat]
___builtin_bswap [definition, in LAProof.C.bandmat]
___builtin_annot_intval [definition, in LAProof.C.bandmat]
___builtin_annot [definition, in LAProof.C.bandmat]
_PR [definition, in LAProof.C.bandmat]
_PA [definition, in LAProof.C.bandmat]
_P [definition, in LAProof.C.bandmat]
_A [definition, in LAProof.C.bandmat]
_t'1 [definition, in LAProof.C.alloc]
_surely_malloc [definition, in LAProof.C.alloc]
_p [definition, in LAProof.C.alloc]
_n [definition, in LAProof.C.alloc]
_malloc [definition, in LAProof.C.alloc]
_main [definition, in LAProof.C.alloc]
_int_calloc [definition, in LAProof.C.alloc]
_i [definition, in LAProof.C.alloc]
_free [definition, in LAProof.C.alloc]
_exit [definition, in LAProof.C.alloc]
_double_clear [definition, in LAProof.C.alloc]
_double_calloc [definition, in LAProof.C.alloc]
___compcert_va_int64 [definition, in LAProof.C.alloc]
___compcert_va_int32 [definition, in LAProof.C.alloc]
___compcert_va_float64 [definition, in LAProof.C.alloc]
___compcert_va_composite [definition, in LAProof.C.alloc]
___compcert_i64_utof [definition, in LAProof.C.alloc]
___compcert_i64_utod [definition, in LAProof.C.alloc]
___compcert_i64_umulh [definition, in LAProof.C.alloc]
___compcert_i64_umod [definition, in LAProof.C.alloc]
___compcert_i64_udiv [definition, in LAProof.C.alloc]
___compcert_i64_stof [definition, in LAProof.C.alloc]
___compcert_i64_stod [definition, in LAProof.C.alloc]
___compcert_i64_smulh [definition, in LAProof.C.alloc]
___compcert_i64_smod [definition, in LAProof.C.alloc]
___compcert_i64_shr [definition, in LAProof.C.alloc]
___compcert_i64_shl [definition, in LAProof.C.alloc]
___compcert_i64_sdiv [definition, in LAProof.C.alloc]
___compcert_i64_sar [definition, in LAProof.C.alloc]
___compcert_i64_dtou [definition, in LAProof.C.alloc]
___compcert_i64_dtos [definition, in LAProof.C.alloc]
___builtin_va_start [definition, in LAProof.C.alloc]
___builtin_va_end [definition, in LAProof.C.alloc]
___builtin_va_copy [definition, in LAProof.C.alloc]
___builtin_va_arg [definition, in LAProof.C.alloc]
___builtin_unreachable [definition, in LAProof.C.alloc]
___builtin_sqrt [definition, in LAProof.C.alloc]
___builtin_sel [definition, in LAProof.C.alloc]
___builtin_memcpy_aligned [definition, in LAProof.C.alloc]
___builtin_membar [definition, in LAProof.C.alloc]
___builtin_fsqrt [definition, in LAProof.C.alloc]
___builtin_fnmsub [definition, in LAProof.C.alloc]
___builtin_fnmadd [definition, in LAProof.C.alloc]
___builtin_fmsub [definition, in LAProof.C.alloc]
___builtin_fmin [definition, in LAProof.C.alloc]
___builtin_fmax [definition, in LAProof.C.alloc]
___builtin_fmadd [definition, in LAProof.C.alloc]
___builtin_fabsf [definition, in LAProof.C.alloc]
___builtin_fabs [definition, in LAProof.C.alloc]
___builtin_expect [definition, in LAProof.C.alloc]
___builtin_debug [definition, in LAProof.C.alloc]
___builtin_ctzll [definition, in LAProof.C.alloc]
___builtin_ctzl [definition, in LAProof.C.alloc]
___builtin_ctz [definition, in LAProof.C.alloc]
___builtin_clzll [definition, in LAProof.C.alloc]
___builtin_clzl [definition, in LAProof.C.alloc]
___builtin_clz [definition, in LAProof.C.alloc]
___builtin_clsll [definition, in LAProof.C.alloc]
___builtin_clsl [definition, in LAProof.C.alloc]
___builtin_cls [definition, in LAProof.C.alloc]
___builtin_bswap64 [definition, in LAProof.C.alloc]
___builtin_bswap32 [definition, in LAProof.C.alloc]
___builtin_bswap16 [definition, in LAProof.C.alloc]
___builtin_bswap [definition, in LAProof.C.alloc]
___builtin_annot_intval [definition, in LAProof.C.alloc]
___builtin_annot [definition, in LAProof.C.alloc]
Module Index
F
F [in LAProof.accuracy_proofs.mv_mathcomp]F [in LAProof.C.spec_densemat]
I
Info [in LAProof.C.sparse]Info [in LAProof.C.densemat]
Info [in LAProof.C.cholesky]
Info [in LAProof.C.bandmat]
Info [in LAProof.C.alloc]
Variable Index
D
DotProdFloat.NAN [in LAProof.accuracy_proofs.dotprod_model]DotProdFloat.t [in LAProof.accuracy_proofs.dotprod_model]
DotProdFMA.NAN [in LAProof.accuracy_proofs.dotprod_model]
DotProdFMA.t [in LAProof.accuracy_proofs.dotprod_model]
F
ForwardErrorRel1.NAN [in LAProof.accuracy_proofs.dot_acc_lemmas]ForwardErrorRel1.t [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.fp [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.Hfin [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.Hfp [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.Hra [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.Hrp [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.NAN [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.rp [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.rp_abs [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.t [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2.vF [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardError.Hfin [in LAProof.accuracy_proofs.dot_acc]
ForwardError.Hfin [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.Hlen [in LAProof.accuracy_proofs.dot_acc]
ForwardError.Hlen [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.NAN [in LAProof.accuracy_proofs.dot_acc]
ForwardError.NAN [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.t [in LAProof.accuracy_proofs.dot_acc]
ForwardError.t [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.v1 [in LAProof.accuracy_proofs.dot_acc]
ForwardError.v1 [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.v2 [in LAProof.accuracy_proofs.dot_acc]
ForwardError.v2 [in LAProof.accuracy_proofs.fma_dot_acc]
F.WithNAN.NAN [in LAProof.accuracy_proofs.mv_mathcomp]
F.WithNAN.t [in LAProof.accuracy_proofs.mv_mathcomp]
G
GenFloat.NAN [in LAProof.accuracy_proofs.float_acc_lems]GenFloat.t [in LAProof.accuracy_proofs.float_acc_lems]
M
MixedErrorRel1.fp [in LAProof.accuracy_proofs.dot_acc_lemmas]MixedErrorRel1.Hfin [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.Hfp [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.Hlen [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.NAN [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.t [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.v1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel1.v2 [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.fp [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.Hfin [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.Hfp [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.Hlen [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.NAN [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.t [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.v1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2.v2 [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedError.Hfin [in LAProof.accuracy_proofs.dot_acc]
MixedError.Hfin [in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.Hlen [in LAProof.accuracy_proofs.dot_acc]
MixedError.Hlen [in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.NAN [in LAProof.accuracy_proofs.dot_acc]
MixedError.NAN [in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.t [in LAProof.accuracy_proofs.dot_acc]
MixedError.t [in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.v1 [in LAProof.accuracy_proofs.dot_acc]
MixedError.v1 [in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.v2 [in LAProof.accuracy_proofs.dot_acc]
MixedError.v2 [in LAProof.accuracy_proofs.fma_dot_acc]
MMERROR.NAN [in LAProof.accuracy_proofs.gemm_acc]
MMERROR.t [in LAProof.accuracy_proofs.gemm_acc]
N
NAN.NAN [in LAProof.accuracy_proofs.fma_is_finite]NAN.t [in LAProof.accuracy_proofs.fma_is_finite]
NonZeroDP.Hlen [in LAProof.accuracy_proofs.dotprod_model]
NonZeroDP.NAN [in LAProof.accuracy_proofs.dotprod_model]
NonZeroDP.t [in LAProof.accuracy_proofs.dotprod_model]
NonZeroDP.v1 [in LAProof.accuracy_proofs.dotprod_model]
NonZeroDP.v2 [in LAProof.accuracy_proofs.dotprod_model]
O
OneNorm.Hfin [in LAProof.accuracy_proofs.vecnorm_acc]OneNorm.NAN [in LAProof.accuracy_proofs.vecnorm_acc]
OneNorm.t [in LAProof.accuracy_proofs.vecnorm_acc]
OneNorm.x [in LAProof.accuracy_proofs.vecnorm_acc]
S
SparseErrorRel1.fp [in LAProof.accuracy_proofs.dot_acc_lemmas]SparseErrorRel1.Hfin [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.Hfp [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.Hlen [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.Hra [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.Hrp [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.NAN [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.rp [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.rp_abs [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.t [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.v1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel1.v2 [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.fp [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.Hfin [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.Hfp [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.Hlen [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.Hra [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.Hrp [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.NAN [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.rp [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.rp_abs [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.t [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.v1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
SparseErrorRel2.v2 [in LAProof.accuracy_proofs.dot_acc_lemmas]
T
TwoNorm.Hfin [in LAProof.accuracy_proofs.vecnorm_acc]TwoNorm.NAN [in LAProof.accuracy_proofs.vecnorm_acc]
TwoNorm.t [in LAProof.accuracy_proofs.vecnorm_acc]
TwoNorm.x [in LAProof.accuracy_proofs.vecnorm_acc]
W
WithNans.NAN [in LAProof.accuracy_proofs.vec_op_acc]WithNans.t [in LAProof.accuracy_proofs.vec_op_acc]
WithNan.NAN [in LAProof.accuracy_proofs.sum_acc]
WithNAN.NAN [in LAProof.accuracy_proofs.gemv_acc]
WithNan.t [in LAProof.accuracy_proofs.sum_acc]
WithNAN.t [in LAProof.accuracy_proofs.gemv_acc]
WithSTD.NAN [in LAProof.accuracy_proofs.sum_model]
WithSTD.NAN [in LAProof.C.verif_cholesky]
WithSTD.STD [in LAProof.C.verif_cholesky]
WithSTD.t [in LAProof.accuracy_proofs.sum_model]
WithSTD.t [in LAProof.C.verif_cholesky]
WithType.NAN [in LAProof.accuracy_proofs.common]
WithType.NAN [in LAProof.accuracy_proofs.common]
WithType.t [in LAProof.accuracy_proofs.common]
WithType.t [in LAProof.accuracy_proofs.common]
Library Index
A
allocB
bandmatC
choleskycommon
D
densematdensemat_lemmas
dotprod_model
dot_acc
dot_acc_lemmas
E
exportF
floatlibfloat_acc_lems
fma_dot_acc
fma_is_finite
G
gemm_accgemv_acc
M
matrix_modelmv_mathcomp
P
preambleS
sparsesparse_model
spec_densemat
spec_alloc
spec_sparse
sum_model
sum_acc
V
vecnorm_accvec_op_acc
verif_densemat
verif_alloc
verif_cholesky
verif_densemat_cholesky
verif_densemat_mult
verif_sparse
verif_sparse_byrows
VSU_densemat
VSU_sparse
Lemma Index
A
about_reptype_ftype [in LAProof.C.spec_densemat]about_the_ctype [in LAProof.C.spec_densemat]
abs_le_rel [in LAProof.accuracy_proofs.common]
all_nth_eq [in LAProof.C.floatlib]
B
BFMA_correct [in LAProof.accuracy_proofs.float_acc_lems]BFMA_finite_e [in LAProof.accuracy_proofs.float_acc_lems]
Bfma_mult_0R [in LAProof.accuracy_proofs.float_acc_lems]
BFMA_eq [in LAProof.C.spec_sparse]
bfVNRM1 [in LAProof.accuracy_proofs.vecnorm_acc]
bfVNRM2 [in LAProof.accuracy_proofs.vecnorm_acc]
big_max_mul [in LAProof.accuracy_proofs.mv_mathcomp]
big_mul [in LAProof.accuracy_proofs.mv_mathcomp]
BMINUS_accurate' [in LAProof.accuracy_proofs.float_acc_lems]
BMINUS_accurate [in LAProof.accuracy_proofs.float_acc_lems]
BMINUS_finite_sub [in LAProof.accuracy_proofs.float_acc_lems]
BMINUS_neg_zero [in LAProof.accuracy_proofs.sum_model]
BMULT_correct [in LAProof.accuracy_proofs.float_acc_lems]
BMULT_finite_e [in LAProof.accuracy_proofs.float_acc_lems]
BMULT_accurate' [in LAProof.accuracy_proofs.float_acc_lems]
BMULT_accurate [in LAProof.accuracy_proofs.float_acc_lems]
Bmult_0R [in LAProof.accuracy_proofs.float_acc_lems]
body_crs_matrix_vector_multiply [in LAProof.C.verif_sparse]
body_double_clear [in LAProof.C.verif_alloc]
body_int_calloc [in LAProof.C.verif_alloc]
body_double_calloc [in LAProof.C.verif_alloc]
body_surely_malloc [in LAProof.C.verif_alloc]
body_densemat_dotprod [in LAProof.C.verif_densemat_mult]
body_densematn_dotprod [in LAProof.C.verif_densemat_mult]
body_densemat_mult [in LAProof.C.verif_densemat_mult]
body_densematn_mult [in LAProof.C.verif_densemat_mult]
body_cholesky [in LAProof.C.verif_cholesky]
body_densemat_csolve [in LAProof.C.verif_densemat_cholesky]
body_densematn_csolve [in LAProof.C.verif_densemat_cholesky]
body_densemat_cfactor [in LAProof.C.verif_densemat_cholesky]
body_densematn_cfactor [in LAProof.C.verif_densemat_cholesky]
body_densemat_norm [in LAProof.C.verif_densemat]
body_densemat_norm2 [in LAProof.C.verif_densemat]
body_data_norm [in LAProof.C.verif_densemat]
body_data_norm2 [in LAProof.C.verif_densemat]
body_densemat_addto [in LAProof.C.verif_densemat]
body_densematn_addto [in LAProof.C.verif_densemat]
body_densemat_set [in LAProof.C.verif_densemat]
body_densematn_set [in LAProof.C.verif_densemat]
body_densemat_get [in LAProof.C.verif_densemat]
body_densematn_get [in LAProof.C.verif_densemat]
body_densemat_clear [in LAProof.C.verif_densemat]
body_densematn_clear [in LAProof.C.verif_densemat]
body_densemat_free [in LAProof.C.verif_densemat]
body_densemat_malloc [in LAProof.C.verif_densemat]
body_crs_matrix_vector_multiply_byrows [in LAProof.C.verif_sparse_byrows]
body_crs_row_vector_multiply [in LAProof.C.verif_sparse_byrows]
body_crs_matrix_rows [in LAProof.C.verif_sparse_byrows]
BPLUS_correct [in LAProof.accuracy_proofs.float_acc_lems]
BPLUS_accurate' [in LAProof.accuracy_proofs.float_acc_lems]
BPLUS_accurate [in LAProof.accuracy_proofs.float_acc_lems]
BPLUS_B2R_zero [in LAProof.accuracy_proofs.float_acc_lems]
BPLUS_finite_e [in LAProof.accuracy_proofs.float_acc_lems]
Bplus_0R [in LAProof.accuracy_proofs.float_acc_lems]
BPLUS_comm [in LAProof.accuracy_proofs.sum_model]
BPLUS_neg_zero [in LAProof.accuracy_proofs.sum_model]
bpow_fprec_lb [in LAProof.accuracy_proofs.fma_is_finite]
bpow_femax_lb [in LAProof.accuracy_proofs.fma_is_finite]
bSUM [in LAProof.accuracy_proofs.sum_acc]
C
check_densemat_layout [in LAProof.C.spec_densemat]cholesky_jik_upto_newrow [in LAProof.C.matrix_model]
cholesky_jik_upto_zero [in LAProof.C.matrix_model]
column_major_const [in LAProof.C.densemat_lemmas]
combine_split [in LAProof.accuracy_proofs.fma_is_finite]
crs_multiply_loop_body [in LAProof.C.verif_sparse]
crs_row_rep_property [in LAProof.C.sparse_model]
crs_row_rep_col_range [in LAProof.C.sparse_model]
crs_row_rep_cols_nonneg [in LAProof.C.sparse_model]
crs_rep_matrix_cols [in LAProof.C.sparse_model]
ctype_of_the_type [in LAProof.C.spec_densemat]
D
default_abs_ge_0 [in LAProof.accuracy_proofs.common]default_abs_gt_0 [in LAProof.accuracy_proofs.common]
default_rel_plus_1_ge_1' [in LAProof.accuracy_proofs.common]
default_rel_plus_1_gt_0 [in LAProof.accuracy_proofs.common]
default_rel_plus_1_gt_1 [in LAProof.accuracy_proofs.common]
default_rel_plus_0_ge_1 [in LAProof.accuracy_proofs.common]
default_rel_plus_1_ge_1 [in LAProof.accuracy_proofs.common]
default_rel_ge_0 [in LAProof.accuracy_proofs.common]
default_rel_gt_0 [in LAProof.accuracy_proofs.common]
default_rel_sep_0 [in LAProof.accuracy_proofs.common]
default_rel_ub [in LAProof.accuracy_proofs.fma_is_finite]
default_abs_ub [in LAProof.accuracy_proofs.fma_is_finite]
defualt_abs_le_fmax [in LAProof.accuracy_proofs.fma_is_finite]
densematn_valid_pointer [in LAProof.C.spec_densemat]
densemat_valid_pointer [in LAProof.C.spec_densemat]
densemat_field_compat0 [in LAProof.C.densemat_lemmas]
dotprodF_rel_fold_right [in LAProof.accuracy_proofs.dotprod_model]
dotprodR_rel_bound'' [in LAProof.accuracy_proofs.dotprod_model]
dotprodR_rel_bound' [in LAProof.accuracy_proofs.dotprod_model]
dotprodR_rev [in LAProof.accuracy_proofs.dotprod_model]
dotprodR_rel_inj [in LAProof.accuracy_proofs.dotprod_model]
dotprodR_rel [in LAProof.accuracy_proofs.dotprod_model]
dotprodR_nil_r [in LAProof.accuracy_proofs.dotprod_model]
dotprodR_nil_l [in LAProof.accuracy_proofs.dotprod_model]
dotprod_forward_error [in LAProof.accuracy_proofs.dot_acc]
dotprod_mixed_error [in LAProof.accuracy_proofs.dot_acc]
dotprod_mixed_error_rel [in LAProof.accuracy_proofs.dot_acc_lemmas]
dotprod_forward_error_rel [in LAProof.accuracy_proofs.dot_acc_lemmas]
dotprod_rel_R_exists_fma [in LAProof.accuracy_proofs.dotprod_model]
dotprod_rel_R_exists [in LAProof.accuracy_proofs.dotprod_model]
dotprod_rel_dotprod_any [in LAProof.accuracy_proofs.dotprod_model]
dotprod_single [in LAProof.accuracy_proofs.dotprod_model]
dotprod_nil_r [in LAProof.accuracy_proofs.dotprod_model]
dotprod_nil_l [in LAProof.accuracy_proofs.dotprod_model]
dotprod_congr [in LAProof.C.floatlib]
dot_prod_rel_nnzR [in LAProof.accuracy_proofs.dotprod_model]
dot_prod_zip_map_Rmult [in LAProof.accuracy_proofs.dotprod_model]
dot_prod_sum_rel_R_Rabs [in LAProof.accuracy_proofs.dotprod_model]
drop_sublist [in LAProof.C.densemat_lemmas]
d_le_g_1 [in LAProof.accuracy_proofs.common]
d_le_g [in LAProof.accuracy_proofs.common]
E
eq_in_subrange [in LAProof.C.matrix_model]exists_mx [in LAProof.accuracy_proofs.mv_mathcomp]
e_le_g1 [in LAProof.accuracy_proofs.common]
F
Faddmx_mixed_error [in LAProof.accuracy_proofs.vec_op_acc]finite_norm2_e [in LAProof.C.floatlib]
finite_dotprod_e [in LAProof.C.floatlib]
finite_sum_from_bounded [in LAProof.accuracy_proofs.fma_is_finite]
firstn_seq [in LAProof.C.densemat_lemmas]
flip_Rplus [in LAProof.accuracy_proofs.dotprod_model]
fma_accurate' [in LAProof.accuracy_proofs.float_acc_lems]
fma_accurate [in LAProof.accuracy_proofs.float_acc_lems]
fma_sparse_dotprod_forward_error [in LAProof.accuracy_proofs.fma_dot_acc]
fma_dotprod_forward_error [in LAProof.accuracy_proofs.fma_dot_acc]
fma_dotprod_mixed_error [in LAProof.accuracy_proofs.fma_dot_acc]
fma_dotprod_mixed_error_rel [in LAProof.accuracy_proofs.dot_acc_lemmas]
fma_dotprod_forward_error_rel [in LAProof.accuracy_proofs.dot_acc_lemmas]
fma_dot_prod_rel_nnzR [in LAProof.accuracy_proofs.dotprod_model]
fma_dot_prod_rel_fold_right [in LAProof.accuracy_proofs.dotprod_model]
fold_crs_rep [in LAProof.C.verif_sparse_byrows]
fold_left_preserves [in LAProof.C.densemat_lemmas]
Fscalemx_mixed_error [in LAProof.accuracy_proofs.vec_op_acc]
fSUM [in LAProof.accuracy_proofs.sum_acc]
Fsum_forward_error [in LAProof.accuracy_proofs.sum_acc]
Fsum_backward_error [in LAProof.accuracy_proofs.sum_acc]
FT2R_Zconst_0 [in LAProof.accuracy_proofs.float_acc_lems]
FT2R_pos_zero [in LAProof.accuracy_proofs.float_acc_lems]
FT2R_neg_zero [in LAProof.accuracy_proofs.float_acc_lems]
FT2R_FR2 [in LAProof.accuracy_proofs.dotprod_model]
fun_bound_pos [in LAProof.accuracy_proofs.fma_is_finite]
fun_bnd_le [in LAProof.accuracy_proofs.fma_is_finite]
fun_bnd_pos_1 [in LAProof.accuracy_proofs.fma_is_finite]
F.dotprod_dotprodF [in LAProof.accuracy_proofs.mv_mathcomp]
F.finitemx_scalemx_e [in LAProof.accuracy_proofs.mv_mathcomp]
F.finitemx_addmx_e [in LAProof.accuracy_proofs.mv_mathcomp]
F.mulmx_dotprodF [in LAProof.accuracy_proofs.mv_mathcomp]
F.mulmx_row [in LAProof.accuracy_proofs.mv_mathcomp]
F.sum_sumF [in LAProof.accuracy_proofs.mv_mathcomp]
G
GEMM_error [in LAProof.accuracy_proofs.gemm_acc]gemv_error [in LAProof.accuracy_proofs.vec_op_acc]
generic_round_property [in LAProof.accuracy_proofs.float_acc_lems]
g_pos [in LAProof.accuracy_proofs.common]
g1n_lt_g1Sn [in LAProof.accuracy_proofs.common]
g1n_le_g1Sn' [in LAProof.accuracy_proofs.common]
g1n_le_g1Sn [in LAProof.accuracy_proofs.common]
g1_pos [in LAProof.accuracy_proofs.common]
I
index_ord_enum [in LAProof.accuracy_proofs.mv_mathcomp]in_take_ord_enum [in LAProof.C.matrix_model]
in_sublist_ord_enum [in LAProof.C.densemat_lemmas]
iota_range [in LAProof.C.verif_cholesky]
iota_plus1 [in LAProof.C.verif_cholesky]
iszeroR_iszeroF [in LAProof.accuracy_proofs.common]
is_finite_minus_no_overflow [in LAProof.accuracy_proofs.float_acc_lems]
is_finite_sum_no_overflow [in LAProof.accuracy_proofs.float_acc_lems]
is_finite_BMULT_no_overflow [in LAProof.accuracy_proofs.float_acc_lems]
is_finite_fma_no_overflow [in LAProof.accuracy_proofs.float_acc_lems]
is_finite_in [in LAProof.accuracy_proofs.sum_model]
is_finite_fma_no_overflow' [in LAProof.accuracy_proofs.fma_is_finite]
L
length_ord_enum [in LAProof.C.matrix_model]length_iota [in LAProof.C.verif_cholesky]
length_split [in LAProof.accuracy_proofs.fma_is_finite]
le_g_Sn [in LAProof.accuracy_proofs.common]
M
map_Rabsp_zip [in LAProof.accuracy_proofs.dotprod_model]map_FR2_zip [in LAProof.accuracy_proofs.dotprod_model]
map_const_ord_enum [in LAProof.C.densemat_lemmas]
matrix_by_index_prop [in LAProof.C.floatlib]
matrix_index_prop [in LAProof.C.floatlib]
matrix_extensionality [in LAProof.C.floatlib]
matrix_extensionality_strong [in LAProof.C.floatlib]
matrix_by_index_index [in LAProof.C.floatlib]
matrix_by_index_cols [in LAProof.C.floatlib]
matrix_by_index_rows [in LAProof.C.floatlib]
mat_axpby_error [in LAProof.accuracy_proofs.gemm_acc]
mat_sum_error [in LAProof.accuracy_proofs.gemm_acc]
mat_vec_mul_forward_error [in LAProof.accuracy_proofs.gemv_acc]
mat_vec_mul_mixed_error [in LAProof.accuracy_proofs.gemv_acc]
maxrA [in LAProof.accuracy_proofs.mv_mathcomp]
maxrC [in LAProof.accuracy_proofs.mv_mathcomp]
MINUS_PLUS_BOPP [in LAProof.accuracy_proofs.sum_model]
MMC_error [in LAProof.accuracy_proofs.gemm_acc]
mult_d_e_g1_le' [in LAProof.accuracy_proofs.common]
mul_mx_row'' [in LAProof.accuracy_proofs.mv_mathcomp]
mul_mx_row' [in LAProof.accuracy_proofs.mv_mathcomp]
N
nan_pl_1 [in LAProof.C.spec_densemat]neg_zero_is_finite [in LAProof.accuracy_proofs.float_acc_lems]
nnzF_is_zero_cons [in LAProof.accuracy_proofs.common]
nnzF_lemma [in LAProof.accuracy_proofs.common]
nnzF_zero [in LAProof.accuracy_proofs.common]
nnzR_cons [in LAProof.accuracy_proofs.common]
nnzR_is_zero_cons [in LAProof.accuracy_proofs.common]
nnzR_lemma [in LAProof.accuracy_proofs.common]
nnzR_zero [in LAProof.accuracy_proofs.common]
normM_pos [in LAProof.accuracy_proofs.mv_mathcomp]
normv_triang [in LAProof.accuracy_proofs.mv_mathcomp]
normv_pos [in LAProof.accuracy_proofs.mv_mathcomp]
norm2_loose_congr [in LAProof.C.floatlib]
norm2_congr [in LAProof.C.floatlib]
norm2_snoc [in LAProof.C.floatlib]
no_overflow_minus_is_finite [in LAProof.accuracy_proofs.float_acc_lems]
no_overflow_sum_is_finite [in LAProof.accuracy_proofs.float_acc_lems]
nth_ord_enum' [in LAProof.C.matrix_model]
nth_ord_enum_lemma [in LAProof.accuracy_proofs.mv_mathcomp]
nth_seq_of_rV [in LAProof.accuracy_proofs.mv_mathcomp]
nth_ord_enum' [in LAProof.accuracy_proofs.mv_mathcomp]
nth_index_enum [in LAProof.accuracy_proofs.mv_mathcomp]
nth_List_nth [in LAProof.accuracy_proofs.mv_mathcomp]
nth_map_inrange [in LAProof.C.floatlib]
nth_map_seq [in LAProof.C.floatlib]
nth_seq_nth [in LAProof.C.densemat_lemmas]
O
one_plus_d_mul_g1' [in LAProof.accuracy_proofs.common]one_plus_d_mul_g1 [in LAProof.accuracy_proofs.common]
one_plus_d_mul_g [in LAProof.accuracy_proofs.common]
ordinal_enum_size [in LAProof.accuracy_proofs.mv_mathcomp]
P
partial_row_next [in LAProof.C.sparse_model]partial_row_end [in LAProof.C.sparse_model]
partial_row_start [in LAProof.C.sparse_model]
plus_e_g1_le [in LAProof.accuracy_proofs.common]
plus_d_e_g1_le [in LAProof.accuracy_proofs.common]
plus_d_e_g1_le' [in LAProof.accuracy_proofs.common]
pred_lt [in LAProof.accuracy_proofs.mv_mathcomp]
R
Rabs_sum [in LAProof.accuracy_proofs.mv_mathcomp]rdiv_mult_eq [in LAProof.accuracy_proofs.fma_is_finite]
rdiv_le [in LAProof.accuracy_proofs.fma_is_finite]
rdiv_lt [in LAProof.accuracy_proofs.fma_is_finite]
Req_eq [in LAProof.accuracy_proofs.dotprod_model]
rev_list_rev [in LAProof.accuracy_proofs.common]
rev_ord_enum [in LAProof.accuracy_proofs.mv_mathcomp]
Rminus_lt_minus [in LAProof.accuracy_proofs.fma_is_finite]
Rminus_le_minus [in LAProof.accuracy_proofs.fma_is_finite]
Rmult_le_lt_compat [in LAProof.accuracy_proofs.common]
round_FT2R [in LAProof.accuracy_proofs.common]
rowmult_app [in LAProof.C.sparse_model]
Rplus_le_lt_compat [in LAProof.accuracy_proofs.common]
Rplus_rewrite [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_nnzR_abs [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_nnzR [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_Rabs_eq [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_single' [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_single [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_fold_right_Rabs' [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_fold_right_Rabs [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_fold_right' [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_fold_right [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_eq [in LAProof.accuracy_proofs.dotprod_model]
S
scaleM_error [in LAProof.accuracy_proofs.gemm_acc]seq_rev_rev [in LAProof.C.densemat_lemmas]
size_not_empty_nat [in LAProof.accuracy_proofs.common]
size_ord_enum [in LAProof.C.matrix_model]
size_seq_of_rV [in LAProof.accuracy_proofs.mv_mathcomp]
size_ord_enum [in LAProof.accuracy_proofs.mv_mathcomp]
Smat_vec_mul_mixed_error [in LAProof.accuracy_proofs.vec_op_acc]
Smat_sumF_mixed_error [in LAProof.accuracy_proofs.vec_op_acc]
sMMC_error [in LAProof.accuracy_proofs.gemm_acc]
sorted_app_e1 [in LAProof.C.sparse_model]
sparse_dotprod_forward_error [in LAProof.accuracy_proofs.dot_acc]
sparse_fma_dotprod_forward_error [in LAProof.accuracy_proofs.dot_acc_lemmas]
sparse_dotprod_forward_error_rel [in LAProof.accuracy_proofs.dot_acc_lemmas]
strict_floatlist_eqv_i [in LAProof.C.sparse_model]
strict_feq_i [in LAProof.C.sparse_model]
subMultNorm [in LAProof.accuracy_proofs.mv_mathcomp]
subtract_another [in LAProof.C.matrix_model]
subtract_loop_sum_any [in LAProof.accuracy_proofs.sum_model]
subtract_loop_sumR [in LAProof.accuracy_proofs.sum_model]
subtract_loop_congr1 [in LAProof.accuracy_proofs.sum_model]
subtract_another [in LAProof.C.verif_cholesky]
sumRabs_Rabs [in LAProof.accuracy_proofs.sum_model]
sumRabs_pos [in LAProof.accuracy_proofs.sum_model]
sumR_sum [in LAProof.accuracy_proofs.mv_mathcomp]
sumR_rev [in LAProof.accuracy_proofs.sum_model]
sumR_permute [in LAProof.accuracy_proofs.sum_model]
sumR_app_cons [in LAProof.accuracy_proofs.sum_model]
sumR_le_sumRabs [in LAProof.accuracy_proofs.sum_model]
sumR_mult [in LAProof.accuracy_proofs.sum_model]
sum_rel_Ft_exists [in LAProof.accuracy_proofs.sum_model]
sum_rel_Ft_fold [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_abs_exists [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_exists [in LAProof.accuracy_proofs.sum_model]
sum_rel_Ft_single [in LAProof.accuracy_proofs.sum_model]
sum_map_Rmult [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_fold [in LAProof.accuracy_proofs.sum_model]
sum_rel_bound'' [in LAProof.accuracy_proofs.sum_model]
sum_rel_bound' [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_permute_t [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_permute [in LAProof.accuracy_proofs.sum_model]
sum_rel_bound [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_app_cons [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_single' [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_single [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_Rabs [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_Rabs_eq [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_Rabs_pos [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_abs [in LAProof.accuracy_proofs.sum_model]
sum_rel_sum_any [in LAProof.accuracy_proofs.sum_model]
sum_rel_R_abs_exists_fma [in LAProof.accuracy_proofs.dotprod_model]
sum_rev [in LAProof.accuracy_proofs.dotprod_model]
sum_forward_error_permute [in LAProof.accuracy_proofs.sum_acc]
sum_forward_error_permute' [in LAProof.accuracy_proofs.sum_acc]
surely_malloc_spec_sub [in LAProof.C.spec_alloc]
T
take_snoc [in LAProof.C.matrix_model]take_sublist [in LAProof.C.densemat_lemmas]
U
update_i_lt_j [in LAProof.C.matrix_model]update_i_lt_j_aux [in LAProof.C.matrix_model]
update_i_lt_j [in LAProof.C.verif_cholesky]
upd_Znth_lists_of_fun [in LAProof.C.verif_cholesky]
upd_Znth_column_major [in LAProof.C.densemat_lemmas]
upto_iota [in LAProof.C.verif_cholesky]
V
val_of_optfloat_column_major [in LAProof.C.densemat_lemmas]vector_sub_congr [in LAProof.C.floatlib]
vec_vec_mul_mixed_error [in LAProof.accuracy_proofs.gemv_acc]
Z
Zlength_iota [in LAProof.C.verif_cholesky]Zlength_seq [in LAProof.C.floatlib]
Zlength_column_major [in LAProof.C.densemat_lemmas]
Zlength_ord_enum [in LAProof.C.densemat_lemmas]
Zmatrix_rows_nat [in LAProof.C.floatlib]
Zmatrix_cols_nat [in LAProof.C.floatlib]
Znth_lists_done [in LAProof.C.verif_cholesky]
Znth_i_list_of_fun [in LAProof.C.verif_cholesky]
Znth_i_iota [in LAProof.C.verif_cholesky]
Znth_vector_sub [in LAProof.C.floatlib]
Znth_column_major [in LAProof.C.densemat_lemmas]
Znth_ord_enum [in LAProof.C.densemat_lemmas]
Axiom Index
B
body_exit [in LAProof.C.verif_alloc]Constructor Index
C
crs_row_rep_val [in LAProof.C.sparse_model]crs_row_rep_zero [in LAProof.C.sparse_model]
crs_row_rep_nil [in LAProof.C.sparse_model]
D
Dotprod_Any_Some [in LAProof.accuracy_proofs.dotprod_model]Dotprod_Any_None [in LAProof.accuracy_proofs.dotprod_model]
Dotprod_Any_perm [in LAProof.accuracy_proofs.dotprod_model]
Dotprod_Any_split [in LAProof.accuracy_proofs.dotprod_model]
Dotprod_Any_1 [in LAProof.accuracy_proofs.dotprod_model]
dot_prod_rel_cons [in LAProof.accuracy_proofs.dotprod_model]
dot_prod_rel_nil [in LAProof.accuracy_proofs.dotprod_model]
F
fma_dot_prod_rel_cons [in LAProof.accuracy_proofs.dotprod_model]fma_dot_prod_rel_nil [in LAProof.accuracy_proofs.dotprod_model]
R
R_dot_prod_rel_cons [in LAProof.accuracy_proofs.dotprod_model]R_dot_prod_rel_nil [in LAProof.accuracy_proofs.dotprod_model]
S
Sum_Any_perm [in LAProof.C.matrix_model]Sum_Any_split [in LAProof.C.matrix_model]
Sum_Any_1 [in LAProof.C.matrix_model]
Sum_Any_0 [in LAProof.C.matrix_model]
Sum_Any_Some [in LAProof.accuracy_proofs.sum_model]
Sum_Any_None [in LAProof.accuracy_proofs.sum_model]
Sum_Any_perm [in LAProof.accuracy_proofs.sum_model]
Sum_Any_split [in LAProof.accuracy_proofs.sum_model]
Sum_Any_1 [in LAProof.accuracy_proofs.sum_model]
sum_rel_cons [in LAProof.accuracy_proofs.sum_model]
sum_rel_nil [in LAProof.accuracy_proofs.sum_model]
Inductive Index
C
crs_row_rep [in LAProof.C.sparse_model]D
dotprod_any [in LAProof.accuracy_proofs.dotprod_model]dotprod_any' [in LAProof.accuracy_proofs.dotprod_model]
dot_prod_rel [in LAProof.accuracy_proofs.dotprod_model]
F
fma_dot_prod_rel [in LAProof.accuracy_proofs.dotprod_model]R
R_dot_prod_rel [in LAProof.accuracy_proofs.dotprod_model]S
sum_any [in LAProof.C.matrix_model]sum_any [in LAProof.accuracy_proofs.sum_model]
sum_any' [in LAProof.accuracy_proofs.sum_model]
sum_rel [in LAProof.accuracy_proofs.sum_model]
Section Index
D
DotProdFloat [in LAProof.accuracy_proofs.dotprod_model]DotProdFMA [in LAProof.accuracy_proofs.dotprod_model]
F
ForwardError [in LAProof.accuracy_proofs.dot_acc]ForwardError [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardErrorRel1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
ForwardErrorRel2 [in LAProof.accuracy_proofs.dot_acc_lemmas]
F.WithNAN [in LAProof.accuracy_proofs.mv_mathcomp]
G
GenFloat [in LAProof.accuracy_proofs.float_acc_lems]M
MixedError [in LAProof.accuracy_proofs.dot_acc]MixedError [in LAProof.accuracy_proofs.fma_dot_acc]
MixedErrorRel1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
MixedErrorRel2 [in LAProof.accuracy_proofs.dot_acc_lemmas]
MMERROR [in LAProof.accuracy_proofs.gemm_acc]
N
NAN [in LAProof.accuracy_proofs.fma_is_finite]NonZeroDP [in LAProof.accuracy_proofs.dotprod_model]
O
OneNorm [in LAProof.accuracy_proofs.vecnorm_acc]R
RealDotProd [in LAProof.accuracy_proofs.dotprod_model]S
SparseErrorRel1 [in LAProof.accuracy_proofs.dot_acc_lemmas]SparseErrorRel2 [in LAProof.accuracy_proofs.dot_acc_lemmas]
T
TwoNorm [in LAProof.accuracy_proofs.vecnorm_acc]W
WithNan [in LAProof.accuracy_proofs.sum_acc]WithNAN [in LAProof.accuracy_proofs.gemv_acc]
WithNans [in LAProof.accuracy_proofs.vec_op_acc]
WithSTD [in LAProof.accuracy_proofs.sum_model]
WithSTD [in LAProof.C.verif_cholesky]
WithType [in LAProof.accuracy_proofs.common]
WithType [in LAProof.accuracy_proofs.common]
Instance Index
C
change_composite_env_alloc' [in LAProof.C.densemat_lemmas]change_composite_env_alloc [in LAProof.C.densemat_lemmas]
CompSpecs [in LAProof.C.spec_densemat]
CompSpecs [in LAProof.C.spec_alloc]
CompSpecs [in LAProof.C.verif_cholesky]
CompSpecs [in LAProof.C.spec_sparse]
M
Malloc [in LAProof.C.spec_alloc]Z
zerof [in LAProof.C.matrix_model]zerof [in LAProof.C.floatlib]
Abbreviation Index
D
D [in LAProof.accuracy_proofs.dot_acc]D [in LAProof.accuracy_proofs.float_acc_lems]
D [in LAProof.accuracy_proofs.fma_dot_acc]
D [in LAProof.accuracy_proofs.common]
D [in LAProof.accuracy_proofs.dot_acc_lemmas]
D [in LAProof.accuracy_proofs.dot_acc_lemmas]
D [in LAProof.accuracy_proofs.dot_acc_lemmas]
D [in LAProof.accuracy_proofs.dot_acc_lemmas]
D [in LAProof.accuracy_proofs.dot_acc_lemmas]
D [in LAProof.accuracy_proofs.sum_acc]
E
E [in LAProof.accuracy_proofs.dot_acc]E [in LAProof.accuracy_proofs.float_acc_lems]
E [in LAProof.accuracy_proofs.fma_dot_acc]
E [in LAProof.accuracy_proofs.common]
E [in LAProof.accuracy_proofs.dot_acc_lemmas]
E [in LAProof.accuracy_proofs.dot_acc_lemmas]
E [in LAProof.accuracy_proofs.dot_acc_lemmas]
E [in LAProof.accuracy_proofs.dot_acc_lemmas]
E [in LAProof.accuracy_proofs.dot_acc_lemmas]
G
g [in LAProof.accuracy_proofs.gemm_acc]g [in LAProof.accuracy_proofs.dot_acc]
g [in LAProof.accuracy_proofs.dot_acc]
g [in LAProof.accuracy_proofs.fma_dot_acc]
g [in LAProof.accuracy_proofs.fma_dot_acc]
g [in LAProof.accuracy_proofs.dot_acc_lemmas]
g [in LAProof.accuracy_proofs.dot_acc_lemmas]
g [in LAProof.accuracy_proofs.dot_acc_lemmas]
g [in LAProof.accuracy_proofs.dot_acc_lemmas]
g [in LAProof.accuracy_proofs.dot_acc_lemmas]
g [in LAProof.accuracy_proofs.dot_acc_lemmas]
g [in LAProof.accuracy_proofs.sum_acc]
g [in LAProof.accuracy_proofs.vec_op_acc]
g [in LAProof.accuracy_proofs.vecnorm_acc]
g [in LAProof.accuracy_proofs.vecnorm_acc]
g [in LAProof.accuracy_proofs.gemv_acc]
g1 [in LAProof.accuracy_proofs.gemm_acc]
g1 [in LAProof.accuracy_proofs.dot_acc]
g1 [in LAProof.accuracy_proofs.dot_acc]
g1 [in LAProof.accuracy_proofs.fma_dot_acc]
g1 [in LAProof.accuracy_proofs.fma_dot_acc]
g1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [in LAProof.accuracy_proofs.dot_acc_lemmas]
g1 [in LAProof.accuracy_proofs.vec_op_acc]
g1 [in LAProof.accuracy_proofs.vecnorm_acc]
g1 [in LAProof.accuracy_proofs.gemv_acc]
N
n [in LAProof.accuracy_proofs.dot_acc]n [in LAProof.accuracy_proofs.fma_dot_acc]
n [in LAProof.accuracy_proofs.vecnorm_acc]
n [in LAProof.accuracy_proofs.vecnorm_acc]
neg_zero [in LAProof.accuracy_proofs.dot_acc]
neg_zero [in LAProof.accuracy_proofs.fma_dot_acc]
neg_zero [in LAProof.accuracy_proofs.fma_dot_acc]
neg_zero [in LAProof.accuracy_proofs.dot_acc_lemmas]
neg_zero [in LAProof.accuracy_proofs.dot_acc_lemmas]
neg_zero [in LAProof.accuracy_proofs.sum_acc]
neg_zero [in LAProof.accuracy_proofs.vecnorm_acc]
neg_zero [in LAProof.accuracy_proofs.vecnorm_acc]
nnzR [in LAProof.accuracy_proofs.dot_acc]
nnzR [in LAProof.accuracy_proofs.fma_dot_acc]
nnzR [in LAProof.accuracy_proofs.dot_acc_lemmas]
nnzR [in LAProof.accuracy_proofs.dot_acc_lemmas]
V
vF [in LAProof.accuracy_proofs.dot_acc_lemmas]vF [in LAProof.accuracy_proofs.dot_acc_lemmas]
vR [in LAProof.accuracy_proofs.dot_acc_lemmas]
vR [in LAProof.accuracy_proofs.dot_acc_lemmas]
vR' [in LAProof.accuracy_proofs.dot_acc_lemmas]
vR' [in LAProof.accuracy_proofs.dot_acc_lemmas]
v1R [in LAProof.accuracy_proofs.dot_acc]
v1R [in LAProof.accuracy_proofs.fma_dot_acc]
v1R [in LAProof.accuracy_proofs.dot_acc_lemmas]
v1R [in LAProof.accuracy_proofs.dot_acc_lemmas]
v1R [in LAProof.accuracy_proofs.dotprod_model]
v1R' [in LAProof.accuracy_proofs.dot_acc]
v1R' [in LAProof.accuracy_proofs.fma_dot_acc]
v2R [in LAProof.accuracy_proofs.dot_acc]
v2R [in LAProof.accuracy_proofs.fma_dot_acc]
v2R' [in LAProof.accuracy_proofs.dot_acc]
v2R' [in LAProof.accuracy_proofs.fma_dot_acc]
X
xR [in LAProof.accuracy_proofs.vecnorm_acc]xR [in LAProof.accuracy_proofs.vecnorm_acc]
Definition Index
A
allocASI [in LAProof.C.spec_alloc]allocVSU [in LAProof.C.verif_alloc]
alloc_internal_specs [in LAProof.C.verif_alloc]
alloc_imported_specs [in LAProof.C.verif_alloc]
alloc_E [in LAProof.C.verif_alloc]
B
backward_subst [in LAProof.C.matrix_model]backward_subst_step [in LAProof.C.matrix_model]
Beq_dec_t [in LAProof.accuracy_proofs.common]
blocksolve_spec [in LAProof.C.spec_densemat]
Bminus_no_overflow [in LAProof.accuracy_proofs.float_acc_lems]
Bmult_no_overflow [in LAProof.accuracy_proofs.float_acc_lems]
Bplus_no_overflow [in LAProof.accuracy_proofs.float_acc_lems]
C
cholesky_jik_ij' [in LAProof.C.matrix_model]cholesky_jik_upto [in LAProof.C.matrix_model]
cholesky_jik_spec [in LAProof.C.matrix_model]
cholesky_jik_ij [in LAProof.C.matrix_model]
cholesky_spec [in LAProof.C.verif_cholesky]
cholesky_jik_upto [in LAProof.C.verif_cholesky]
cholesky_jik_spec [in LAProof.C.verif_cholesky]
cholesky_jik_ij [in LAProof.C.verif_cholesky]
column_major [in LAProof.C.spec_densemat]
composites [in LAProof.C.sparse]
composites [in LAProof.C.densemat]
composites [in LAProof.C.cholesky]
composites [in LAProof.C.bandmat]
composites [in LAProof.C.alloc]
crazy [in LAProof.accuracy_proofs.mv_mathcomp]
crs_matrix_vector_multiply_spec [in LAProof.C.spec_sparse]
crs_matrix_vector_multiply_byrows_spec [in LAProof.C.spec_sparse]
crs_row_vector_multiply_spec [in LAProof.C.spec_sparse]
crs_matrix_rows_spec [in LAProof.C.spec_sparse]
crs_rep [in LAProof.C.spec_sparse]
crs_rep_aux [in LAProof.C.sparse_model]
crs_row_rep_sind [in LAProof.C.sparse_model]
crs_row_rep_ind [in LAProof.C.sparse_model]
ctype_of_type [in LAProof.C.spec_densemat]
D
data_norm_spec [in LAProof.C.spec_densemat]data_norm2_spec [in LAProof.C.spec_densemat]
default_abs [in LAProof.accuracy_proofs.common]
default_rel [in LAProof.accuracy_proofs.common]
densemat [in LAProof.C.spec_densemat]
densematASI [in LAProof.C.spec_densemat]
densematn [in LAProof.C.spec_densemat]
densematn_cfactor_outer_spec [in LAProof.C.spec_densemat]
densematn_cfactor_block_spec [in LAProof.C.spec_densemat]
densematn_lusolveT_spec [in LAProof.C.spec_densemat]
densematn_lufactor_spec [in LAProof.C.spec_densemat]
densematn_lusolve_spec [in LAProof.C.spec_densemat]
densematn_print_spec [in LAProof.C.spec_densemat]
densematn_lujac_spec [in LAProof.C.spec_densemat]
densematn_mult_spec [in LAProof.C.spec_densemat]
densematn_dotprod_spec [in LAProof.C.spec_densemat]
densematn_csolve_spec [in LAProof.C.spec_densemat]
densematn_cfactor_spec [in LAProof.C.spec_densemat]
densematn_addto_spec [in LAProof.C.spec_densemat]
densematn_set_spec [in LAProof.C.spec_densemat]
densematn_get_spec [in LAProof.C.spec_densemat]
densematn_clear_spec [in LAProof.C.spec_densemat]
densematn_local_facts [in LAProof.C.spec_densemat]
densematVSU [in LAProof.C.VSU_densemat]
densemat_lusolveT_spec [in LAProof.C.spec_densemat]
densemat_lufactor_spec [in LAProof.C.spec_densemat]
densemat_lusolve_spec [in LAProof.C.spec_densemat]
densemat_print_spec [in LAProof.C.spec_densemat]
densemat_lujac_spec [in LAProof.C.spec_densemat]
densemat_mult_spec [in LAProof.C.spec_densemat]
densemat_dotprod_spec [in LAProof.C.spec_densemat]
densemat_csolve_spec [in LAProof.C.spec_densemat]
densemat_cfactor_spec [in LAProof.C.spec_densemat]
densemat_norm_spec [in LAProof.C.spec_densemat]
densemat_norm2_spec [in LAProof.C.spec_densemat]
densemat_addto_spec [in LAProof.C.spec_densemat]
densemat_set_spec [in LAProof.C.spec_densemat]
densemat_get_spec [in LAProof.C.spec_densemat]
densemat_clear_spec [in LAProof.C.spec_densemat]
densemat_free_spec [in LAProof.C.spec_densemat]
densemat_malloc_spec [in LAProof.C.spec_densemat]
densemat_local_facts [in LAProof.C.spec_densemat]
densemat_data_offset [in LAProof.C.spec_densemat]
densemat_t [in LAProof.C.spec_densemat]
densemat_internal_specs [in LAProof.C.densemat_lemmas]
densemat_imported_specs [in LAProof.C.densemat_lemmas]
densemat_E [in LAProof.C.densemat_lemmas]
done_to_n [in LAProof.C.verif_cholesky]
done_to_ij [in LAProof.C.verif_cholesky]
dotprod [in LAProof.accuracy_proofs.dotprod_model]
dotprod [in LAProof.C.floatlib]
dotprodF [in LAProof.accuracy_proofs.dotprod_model]
dotprodR [in LAProof.accuracy_proofs.dotprod_model]
dotprod_any_sind [in LAProof.accuracy_proofs.dotprod_model]
dotprod_any_ind [in LAProof.accuracy_proofs.dotprod_model]
dotprod_any'_sind [in LAProof.accuracy_proofs.dotprod_model]
dotprod_any'_ind [in LAProof.accuracy_proofs.dotprod_model]
dot_prod_rel_sind [in LAProof.accuracy_proofs.dotprod_model]
dot_prod_rel_ind [in LAProof.accuracy_proofs.dotprod_model]
double_clear_spec [in LAProof.C.spec_alloc]
double_calloc_spec [in LAProof.C.spec_alloc]
E
exit_spec [in LAProof.C.spec_alloc]F
fmax [in LAProof.accuracy_proofs.fma_is_finite]fma_no_overflow [in LAProof.accuracy_proofs.float_acc_lems]
fma_dot_prod_rel_sind [in LAProof.accuracy_proofs.dotprod_model]
fma_dot_prod_rel_ind [in LAProof.accuracy_proofs.dotprod_model]
fma_dotprod [in LAProof.accuracy_proofs.dotprod_model]
forward_subst [in LAProof.C.matrix_model]
forward_subst_step [in LAProof.C.matrix_model]
frobenius_norm [in LAProof.C.spec_densemat]
frobenius_norm2 [in LAProof.C.spec_densemat]
FR2 [in LAProof.accuracy_proofs.dotprod_model]
fun_bnd [in LAProof.accuracy_proofs.fma_is_finite]
f_crs_matrix_rows [in LAProof.C.sparse]
f_crs_matrix_vector_multiply [in LAProof.C.sparse]
f_crs_matrix_vector_multiply_byrows [in LAProof.C.sparse]
f_crs_row_vector_multiply [in LAProof.C.sparse]
f_densemat_mult [in LAProof.C.densemat]
f_densematn_mult [in LAProof.C.densemat]
f_densemat_dotprod [in LAProof.C.densemat]
f_densematn_dotprod [in LAProof.C.densemat]
f_densemat_norm [in LAProof.C.densemat]
f_densemat_norm2 [in LAProof.C.densemat]
f_data_norm [in LAProof.C.densemat]
f_data_norm2 [in LAProof.C.densemat]
f_densemat_lujac [in LAProof.C.densemat]
f_densemat_lusolveT [in LAProof.C.densemat]
f_densemat_lusolve [in LAProof.C.densemat]
f_densemat_lufactor [in LAProof.C.densemat]
f_densematn_lujac [in LAProof.C.densemat]
f_densematn_lusolveT [in LAProof.C.densemat]
f_densematn_lusolve [in LAProof.C.densemat]
f_densematn_lufactor [in LAProof.C.densemat]
f_densemat_csolve [in LAProof.C.densemat]
f_densematn_csolve [in LAProof.C.densemat]
f_densemat_cfactor [in LAProof.C.densemat]
f_densematn_cfactor_block [in LAProof.C.densemat]
f_subtractoff [in LAProof.C.densemat]
f_blocksolve [in LAProof.C.densemat]
f_densematn_cfactor_outer [in LAProof.C.densemat]
f_densematn_cfactor [in LAProof.C.densemat]
f_densemat_print [in LAProof.C.densemat]
f_densematn_print [in LAProof.C.densemat]
f_densemat_addto [in LAProof.C.densemat]
f_densemat_set [in LAProof.C.densemat]
f_densemat_get [in LAProof.C.densemat]
f_densematn_addto [in LAProof.C.densemat]
f_densematn_set [in LAProof.C.densemat]
f_densematn_get [in LAProof.C.densemat]
f_densemat_clear [in LAProof.C.densemat]
f_densematn_clear [in LAProof.C.densemat]
f_densemat_free [in LAProof.C.densemat]
f_densemat_malloc [in LAProof.C.densemat]
f_cholesky [in LAProof.C.cholesky]
f_bandmat_norm [in LAProof.C.bandmat]
f_bandmat_norm2 [in LAProof.C.bandmat]
f_bandmat_solve [in LAProof.C.bandmat]
f_bandmat_factor [in LAProof.C.bandmat]
f_bandmat_print [in LAProof.C.bandmat]
f_dense_to_band [in LAProof.C.bandmat]
f_bandmat_addto [in LAProof.C.bandmat]
f_bandmat_set [in LAProof.C.bandmat]
f_bandmat_get [in LAProof.C.bandmat]
f_bandmatn_addto [in LAProof.C.bandmat]
f_bandmatn_set [in LAProof.C.bandmat]
f_bandmatn_get [in LAProof.C.bandmat]
f_bandmat_clear [in LAProof.C.bandmat]
f_bandmatn_clear [in LAProof.C.bandmat]
f_bandmat_free [in LAProof.C.bandmat]
f_bandmat_malloc [in LAProof.C.bandmat]
f_int_calloc [in LAProof.C.alloc]
f_double_calloc [in LAProof.C.alloc]
f_double_clear [in LAProof.C.alloc]
f_surely_malloc [in LAProof.C.alloc]
F.addmx [in LAProof.accuracy_proofs.mv_mathcomp]
F.dotprod [in LAProof.accuracy_proofs.mv_mathcomp]
F.finitemx [in LAProof.accuracy_proofs.mv_mathcomp]
F.mulmx [in LAProof.accuracy_proofs.mv_mathcomp]
F.scalemx [in LAProof.accuracy_proofs.mv_mathcomp]
F.sum [in LAProof.accuracy_proofs.mv_mathcomp]
G
g [in LAProof.accuracy_proofs.common]global_definitions [in LAProof.C.sparse]
global_definitions [in LAProof.C.densemat]
global_definitions [in LAProof.C.cholesky]
global_definitions [in LAProof.C.bandmat]
global_definitions [in LAProof.C.alloc]
Gprog [in LAProof.C.verif_alloc]
Gprog [in LAProof.C.verif_cholesky]
Gprog [in LAProof.C.spec_sparse]
Gprog [in LAProof.C.densemat_lemmas]
g1 [in LAProof.accuracy_proofs.common]
I
Info.abi [in LAProof.C.sparse]Info.abi [in LAProof.C.densemat]
Info.abi [in LAProof.C.cholesky]
Info.abi [in LAProof.C.bandmat]
Info.abi [in LAProof.C.alloc]
Info.arch [in LAProof.C.sparse]
Info.arch [in LAProof.C.densemat]
Info.arch [in LAProof.C.cholesky]
Info.arch [in LAProof.C.bandmat]
Info.arch [in LAProof.C.alloc]
Info.big_endian [in LAProof.C.sparse]
Info.big_endian [in LAProof.C.densemat]
Info.big_endian [in LAProof.C.cholesky]
Info.big_endian [in LAProof.C.bandmat]
Info.big_endian [in LAProof.C.alloc]
Info.bitsize [in LAProof.C.sparse]
Info.bitsize [in LAProof.C.densemat]
Info.bitsize [in LAProof.C.cholesky]
Info.bitsize [in LAProof.C.bandmat]
Info.bitsize [in LAProof.C.alloc]
Info.build_branch [in LAProof.C.sparse]
Info.build_tag [in LAProof.C.sparse]
Info.build_number [in LAProof.C.sparse]
Info.build_branch [in LAProof.C.densemat]
Info.build_tag [in LAProof.C.densemat]
Info.build_number [in LAProof.C.densemat]
Info.build_branch [in LAProof.C.cholesky]
Info.build_tag [in LAProof.C.cholesky]
Info.build_number [in LAProof.C.cholesky]
Info.build_branch [in LAProof.C.bandmat]
Info.build_tag [in LAProof.C.bandmat]
Info.build_number [in LAProof.C.bandmat]
Info.build_branch [in LAProof.C.alloc]
Info.build_tag [in LAProof.C.alloc]
Info.build_number [in LAProof.C.alloc]
Info.model [in LAProof.C.sparse]
Info.model [in LAProof.C.densemat]
Info.model [in LAProof.C.cholesky]
Info.model [in LAProof.C.bandmat]
Info.model [in LAProof.C.alloc]
Info.normalized [in LAProof.C.sparse]
Info.normalized [in LAProof.C.densemat]
Info.normalized [in LAProof.C.cholesky]
Info.normalized [in LAProof.C.bandmat]
Info.normalized [in LAProof.C.alloc]
Info.source_file [in LAProof.C.sparse]
Info.source_file [in LAProof.C.densemat]
Info.source_file [in LAProof.C.cholesky]
Info.source_file [in LAProof.C.bandmat]
Info.source_file [in LAProof.C.alloc]
Info.version [in LAProof.C.sparse]
Info.version [in LAProof.C.densemat]
Info.version [in LAProof.C.cholesky]
Info.version [in LAProof.C.bandmat]
Info.version [in LAProof.C.alloc]
int_calloc_spec [in LAProof.C.spec_alloc]
iota [in LAProof.C.verif_cholesky]
iszero [in LAProof.accuracy_proofs.common]
J
joinLU [in LAProof.C.matrix_model]L
lists_of_fun [in LAProof.C.verif_cholesky]list_of_fun [in LAProof.C.verif_cholesky]
lshift1 [in LAProof.C.matrix_model]
M
map2 [in LAProof.C.floatlib]matrix [in LAProof.C.verif_cholesky]
matrix [in LAProof.C.floatlib]
matrix_cols_nat [in LAProof.C.floatlib]
matrix_rows_nat [in LAProof.C.floatlib]
matrix_by_index [in LAProof.C.floatlib]
matrix_index [in LAProof.C.floatlib]
matrix_add [in LAProof.C.floatlib]
matrix_rows [in LAProof.C.floatlib]
matrix_cols [in LAProof.C.floatlib]
matrix_matrix_mult [in LAProof.C.floatlib]
matrix_vector_mult [in LAProof.C.floatlib]
mirror_UT [in LAProof.C.matrix_model]
N
N [in LAProof.C.verif_cholesky]nan1 [in LAProof.C.spec_densemat]
neg_zero [in LAProof.accuracy_proofs.common]
neg_zero [in LAProof.C.matrix_model]
neg_zero [in LAProof.C.verif_cholesky]
nnzF [in LAProof.accuracy_proofs.common]
nnzR [in LAProof.accuracy_proofs.common]
normM [in LAProof.accuracy_proofs.mv_mathcomp]
normv [in LAProof.accuracy_proofs.mv_mathcomp]
norm2 [in LAProof.C.floatlib]
N_eq [in LAProof.C.verif_cholesky]
O
one_normR [in LAProof.accuracy_proofs.vecnorm_acc]one_normF [in LAProof.accuracy_proofs.vecnorm_acc]
opp_matrix [in LAProof.C.floatlib]
optfloat_to_float [in LAProof.C.spec_densemat]
P
partial_row [in LAProof.C.sparse_model]pos_zero [in LAProof.accuracy_proofs.common]
pred_ord [in LAProof.accuracy_proofs.mv_mathcomp]
prog [in LAProof.C.sparse]
prog [in LAProof.C.densemat]
prog [in LAProof.C.cholesky]
prog [in LAProof.C.bandmat]
prog [in LAProof.C.alloc]
public_idents [in LAProof.C.sparse]
public_idents [in LAProof.C.densemat]
public_idents [in LAProof.C.cholesky]
public_idents [in LAProof.C.bandmat]
public_idents [in LAProof.C.alloc]
R
Rabsp [in LAProof.accuracy_proofs.dotprod_model]reptype_ftype [in LAProof.C.spec_densemat]
rounded [in LAProof.accuracy_proofs.common]
rowmult [in LAProof.C.sparse_model]
R_dot_prod_rel_sind [in LAProof.accuracy_proofs.dotprod_model]
R_dot_prod_rel_ind [in LAProof.accuracy_proofs.dotprod_model]
S
seq_of_rV [in LAProof.accuracy_proofs.mv_mathcomp]SparseASI [in LAProof.C.spec_sparse]
sparseImports [in LAProof.C.VSU_sparse]
SparseVSU [in LAProof.C.VSU_sparse]
SubsetMathASI [in LAProof.C.spec_sparse]
subtractoff_spec [in LAProof.C.spec_densemat]
subtract_loop' [in LAProof.C.matrix_model]
subtract_loop [in LAProof.C.matrix_model]
subtract_loop [in LAProof.accuracy_proofs.sum_model]
subtract_loop [in LAProof.C.verif_cholesky]
sumF [in LAProof.accuracy_proofs.sum_model]
sumF [in LAProof.C.verif_cholesky]
sumR [in LAProof.accuracy_proofs.sum_model]
sum_any_sind [in LAProof.C.matrix_model]
sum_any_ind [in LAProof.C.matrix_model]
sum_abs [in LAProof.accuracy_proofs.mv_mathcomp]
sum_rel_Ft [in LAProof.accuracy_proofs.sum_model]
sum_any_sind [in LAProof.accuracy_proofs.sum_model]
sum_any_ind [in LAProof.accuracy_proofs.sum_model]
sum_any'_sind [in LAProof.accuracy_proofs.sum_model]
sum_any'_ind [in LAProof.accuracy_proofs.sum_model]
sum_rel_R [in LAProof.accuracy_proofs.sum_model]
sum_rel_sind [in LAProof.accuracy_proofs.sum_model]
sum_rel_ind [in LAProof.accuracy_proofs.sum_model]
sum_upto [in LAProof.C.verif_cholesky]
sum_fold [in LAProof.accuracy_proofs.dotprod_model]
surely_malloc_spec [in LAProof.C.spec_alloc]
surely_malloc_spec' [in LAProof.C.spec_alloc]
T
the_loop_body [in LAProof.C.verif_sparse]the_type [in LAProof.C.spec_densemat]
the_ctype [in LAProof.C.spec_densemat]
two_normR [in LAProof.accuracy_proofs.vecnorm_acc]
two_normF [in LAProof.accuracy_proofs.vecnorm_acc]
t_crs [in LAProof.C.spec_sparse]
U
update_mx [in LAProof.C.matrix_model]updij [in LAProof.C.verif_cholesky]
upto_row_col [in LAProof.C.verif_densemat_mult]
V
val_of_optfloat [in LAProof.C.spec_densemat]val_of_float [in LAProof.C.spec_densemat]
vector [in LAProof.C.floatlib]
vector_sub [in LAProof.C.floatlib]
vector_add [in LAProof.C.floatlib]
Vprog [in LAProof.C.spec_densemat]
Vprog [in LAProof.C.spec_alloc]
Vprog [in LAProof.C.verif_cholesky]
Vprog [in LAProof.C.spec_sparse]
v___stringlit_2 [in LAProof.C.densemat]
v___stringlit_5 [in LAProof.C.densemat]
v___stringlit_3 [in LAProof.C.densemat]
v___stringlit_7 [in LAProof.C.densemat]
v___stringlit_6 [in LAProof.C.densemat]
v___stringlit_4 [in LAProof.C.densemat]
v___stringlit_1 [in LAProof.C.densemat]
v___stringlit_4 [in LAProof.C.bandmat]
v___stringlit_2 [in LAProof.C.bandmat]
v___stringlit_5 [in LAProof.C.bandmat]
v___stringlit_1 [in LAProof.C.bandmat]
v___stringlit_3 [in LAProof.C.bandmat]
_
_t'2 [in LAProof.C.sparse]_t'1 [in LAProof.C.sparse]
_y [in LAProof.C.sparse]
_x [in LAProof.C.sparse]
_val [in LAProof.C.sparse]
_v [in LAProof.C.sparse]
_s [in LAProof.C.sparse]
_rows [in LAProof.C.sparse]
_row_ptr [in LAProof.C.sparse]
_p [in LAProof.C.sparse]
_next [in LAProof.C.sparse]
_main [in LAProof.C.sparse]
_m [in LAProof.C.sparse]
_j [in LAProof.C.sparse]
_i [in LAProof.C.sparse]
_hi [in LAProof.C.sparse]
_h [in LAProof.C.sparse]
_fma [in LAProof.C.sparse]
_crs_row_vector_multiply [in LAProof.C.sparse]
_crs_matrix_vector_multiply_byrows [in LAProof.C.sparse]
_crs_matrix_vector_multiply [in LAProof.C.sparse]
_crs_matrix_rows [in LAProof.C.sparse]
_crs_matrix [in LAProof.C.sparse]
_cols [in LAProof.C.sparse]
_col_ind [in LAProof.C.sparse]
___compcert_va_int64 [in LAProof.C.sparse]
___compcert_va_int32 [in LAProof.C.sparse]
___compcert_va_float64 [in LAProof.C.sparse]
___compcert_va_composite [in LAProof.C.sparse]
___compcert_i64_utof [in LAProof.C.sparse]
___compcert_i64_utod [in LAProof.C.sparse]
___compcert_i64_umulh [in LAProof.C.sparse]
___compcert_i64_umod [in LAProof.C.sparse]
___compcert_i64_udiv [in LAProof.C.sparse]
___compcert_i64_stof [in LAProof.C.sparse]
___compcert_i64_stod [in LAProof.C.sparse]
___compcert_i64_smulh [in LAProof.C.sparse]
___compcert_i64_smod [in LAProof.C.sparse]
___compcert_i64_shr [in LAProof.C.sparse]
___compcert_i64_shl [in LAProof.C.sparse]
___compcert_i64_sdiv [in LAProof.C.sparse]
___compcert_i64_sar [in LAProof.C.sparse]
___compcert_i64_dtou [in LAProof.C.sparse]
___compcert_i64_dtos [in LAProof.C.sparse]
___builtin_va_start [in LAProof.C.sparse]
___builtin_va_end [in LAProof.C.sparse]
___builtin_va_copy [in LAProof.C.sparse]
___builtin_va_arg [in LAProof.C.sparse]
___builtin_unreachable [in LAProof.C.sparse]
___builtin_sqrt [in LAProof.C.sparse]
___builtin_sel [in LAProof.C.sparse]
___builtin_memcpy_aligned [in LAProof.C.sparse]
___builtin_membar [in LAProof.C.sparse]
___builtin_fsqrt [in LAProof.C.sparse]
___builtin_fnmsub [in LAProof.C.sparse]
___builtin_fnmadd [in LAProof.C.sparse]
___builtin_fmsub [in LAProof.C.sparse]
___builtin_fmin [in LAProof.C.sparse]
___builtin_fmax [in LAProof.C.sparse]
___builtin_fmadd [in LAProof.C.sparse]
___builtin_fabsf [in LAProof.C.sparse]
___builtin_fabs [in LAProof.C.sparse]
___builtin_expect [in LAProof.C.sparse]
___builtin_debug [in LAProof.C.sparse]
___builtin_ctzll [in LAProof.C.sparse]
___builtin_ctzl [in LAProof.C.sparse]
___builtin_ctz [in LAProof.C.sparse]
___builtin_clzll [in LAProof.C.sparse]
___builtin_clzl [in LAProof.C.sparse]
___builtin_clz [in LAProof.C.sparse]
___builtin_clsll [in LAProof.C.sparse]
___builtin_clsl [in LAProof.C.sparse]
___builtin_cls [in LAProof.C.sparse]
___builtin_bswap64 [in LAProof.C.sparse]
___builtin_bswap32 [in LAProof.C.sparse]
___builtin_bswap16 [in LAProof.C.sparse]
___builtin_bswap [in LAProof.C.sparse]
___builtin_annot_intval [in LAProof.C.sparse]
___builtin_annot [in LAProof.C.sparse]
_t'9 [in LAProof.C.densemat]
_t'8 [in LAProof.C.densemat]
_t'7 [in LAProof.C.densemat]
_t'6 [in LAProof.C.densemat]
_t'5 [in LAProof.C.densemat]
_t'4 [in LAProof.C.densemat]
_t'3 [in LAProof.C.densemat]
_t'2 [in LAProof.C.densemat]
_t'10 [in LAProof.C.densemat]
_t'1 [in LAProof.C.densemat]
_z [in LAProof.C.densemat]
_yi [in LAProof.C.densemat]
_y [in LAProof.C.densemat]
_xj [in LAProof.C.densemat]
_x [in LAProof.C.densemat]
_vm [in LAProof.C.densemat]
_t [in LAProof.C.densemat]
_surely_malloc [in LAProof.C.densemat]
_subtractoff [in LAProof.C.densemat]
_sqrt [in LAProof.C.densemat]
_s [in LAProof.C.densemat]
_rows [in LAProof.C.densemat]
_rkk [in LAProof.C.densemat]
_rkj [in LAProof.C.densemat]
_result [in LAProof.C.densemat]
_printf [in LAProof.C.densemat]
_p [in LAProof.C.densemat]
_nswap [in LAProof.C.densemat]
_n [in LAProof.C.densemat]
_main [in LAProof.C.densemat]
_m [in LAProof.C.densemat]
_l [in LAProof.C.densemat]
_k__1 [in LAProof.C.densemat]
_k [in LAProof.C.densemat]
_j__1 [in LAProof.C.densemat]
_j [in LAProof.C.densemat]
_ipivj [in LAProof.C.densemat]
_ipiv [in LAProof.C.densemat]
_i__2 [in LAProof.C.densemat]
_i__1 [in LAProof.C.densemat]
_i [in LAProof.C.densemat]
_h [in LAProof.C.densemat]
_free [in LAProof.C.densemat]
_fma [in LAProof.C.densemat]
_fabs [in LAProof.C.densemat]
_double_clear [in LAProof.C.densemat]
_dm [in LAProof.C.densemat]
_densematn_set [in LAProof.C.densemat]
_densematn_print [in LAProof.C.densemat]
_densematn_mult [in LAProof.C.densemat]
_densematn_lusolveT [in LAProof.C.densemat]
_densematn_lusolve [in LAProof.C.densemat]
_densematn_lujac [in LAProof.C.densemat]
_densematn_lufactor [in LAProof.C.densemat]
_densematn_get [in LAProof.C.densemat]
_densematn_dotprod [in LAProof.C.densemat]
_densematn_csolve [in LAProof.C.densemat]
_densematn_clear [in LAProof.C.densemat]
_densematn_cfactor_outer [in LAProof.C.densemat]
_densematn_cfactor_block [in LAProof.C.densemat]
_densematn_cfactor [in LAProof.C.densemat]
_densematn_addto [in LAProof.C.densemat]
_densemat_t [in LAProof.C.densemat]
_densemat_set [in LAProof.C.densemat]
_densemat_print [in LAProof.C.densemat]
_densemat_norm2 [in LAProof.C.densemat]
_densemat_norm [in LAProof.C.densemat]
_densemat_mult [in LAProof.C.densemat]
_densemat_malloc [in LAProof.C.densemat]
_densemat_lusolveT [in LAProof.C.densemat]
_densemat_lusolve [in LAProof.C.densemat]
_densemat_lujac [in LAProof.C.densemat]
_densemat_lufactor [in LAProof.C.densemat]
_densemat_get [in LAProof.C.densemat]
_densemat_free [in LAProof.C.densemat]
_densemat_dotprod [in LAProof.C.densemat]
_densemat_csolve [in LAProof.C.densemat]
_densemat_clear [in LAProof.C.densemat]
_densemat_cfactor [in LAProof.C.densemat]
_densemat_addto [in LAProof.C.densemat]
_data_norm2 [in LAProof.C.densemat]
_data_norm [in LAProof.C.densemat]
_data [in LAProof.C.densemat]
_c [in LAProof.C.densemat]
_blocksolve [in LAProof.C.densemat]
_bi [in LAProof.C.densemat]
_b [in LAProof.C.densemat]
_akk [in LAProof.C.densemat]
_abort [in LAProof.C.densemat]
___stringlit_7 [in LAProof.C.densemat]
___stringlit_6 [in LAProof.C.densemat]
___stringlit_5 [in LAProof.C.densemat]
___stringlit_4 [in LAProof.C.densemat]
___stringlit_3 [in LAProof.C.densemat]
___stringlit_2 [in LAProof.C.densemat]
___stringlit_1 [in LAProof.C.densemat]
___compcert_va_int64 [in LAProof.C.densemat]
___compcert_va_int32 [in LAProof.C.densemat]
___compcert_va_float64 [in LAProof.C.densemat]
___compcert_va_composite [in LAProof.C.densemat]
___compcert_i64_utof [in LAProof.C.densemat]
___compcert_i64_utod [in LAProof.C.densemat]
___compcert_i64_umulh [in LAProof.C.densemat]
___compcert_i64_umod [in LAProof.C.densemat]
___compcert_i64_udiv [in LAProof.C.densemat]
___compcert_i64_stof [in LAProof.C.densemat]
___compcert_i64_stod [in LAProof.C.densemat]
___compcert_i64_smulh [in LAProof.C.densemat]
___compcert_i64_smod [in LAProof.C.densemat]
___compcert_i64_shr [in LAProof.C.densemat]
___compcert_i64_shl [in LAProof.C.densemat]
___compcert_i64_sdiv [in LAProof.C.densemat]
___compcert_i64_sar [in LAProof.C.densemat]
___compcert_i64_dtou [in LAProof.C.densemat]
___compcert_i64_dtos [in LAProof.C.densemat]
___builtin_va_start [in LAProof.C.densemat]
___builtin_va_end [in LAProof.C.densemat]
___builtin_va_copy [in LAProof.C.densemat]
___builtin_va_arg [in LAProof.C.densemat]
___builtin_unreachable [in LAProof.C.densemat]
___builtin_sqrt [in LAProof.C.densemat]
___builtin_sel [in LAProof.C.densemat]
___builtin_memcpy_aligned [in LAProof.C.densemat]
___builtin_membar [in LAProof.C.densemat]
___builtin_fsqrt [in LAProof.C.densemat]
___builtin_fnmsub [in LAProof.C.densemat]
___builtin_fnmadd [in LAProof.C.densemat]
___builtin_fmsub [in LAProof.C.densemat]
___builtin_fmin [in LAProof.C.densemat]
___builtin_fmax [in LAProof.C.densemat]
___builtin_fmadd [in LAProof.C.densemat]
___builtin_fabsf [in LAProof.C.densemat]
___builtin_fabs [in LAProof.C.densemat]
___builtin_expect [in LAProof.C.densemat]
___builtin_debug [in LAProof.C.densemat]
___builtin_ctzll [in LAProof.C.densemat]
___builtin_ctzl [in LAProof.C.densemat]
___builtin_ctz [in LAProof.C.densemat]
___builtin_clzll [in LAProof.C.densemat]
___builtin_clzl [in LAProof.C.densemat]
___builtin_clz [in LAProof.C.densemat]
___builtin_clsll [in LAProof.C.densemat]
___builtin_clsl [in LAProof.C.densemat]
___builtin_cls [in LAProof.C.densemat]
___builtin_bswap64 [in LAProof.C.densemat]
___builtin_bswap32 [in LAProof.C.densemat]
___builtin_bswap16 [in LAProof.C.densemat]
___builtin_bswap [in LAProof.C.densemat]
___builtin_annot_intval [in LAProof.C.densemat]
___builtin_annot [in LAProof.C.densemat]
_Ujk [in LAProof.C.densemat]
_Ujj [in LAProof.C.densemat]
_R [in LAProof.C.densemat]
_Lij [in LAProof.C.densemat]
_J [in LAProof.C.densemat]
_A [in LAProof.C.densemat]
_t'4 [in LAProof.C.cholesky]
_t'3 [in LAProof.C.cholesky]
_t'2 [in LAProof.C.cholesky]
_t'1 [in LAProof.C.cholesky]
_sqrt [in LAProof.C.cholesky]
_s [in LAProof.C.cholesky]
_rkj [in LAProof.C.cholesky]
_n [in LAProof.C.cholesky]
_main [in LAProof.C.cholesky]
_k [in LAProof.C.cholesky]
_j [in LAProof.C.cholesky]
_i [in LAProof.C.cholesky]
_cholesky [in LAProof.C.cholesky]
___compcert_va_int64 [in LAProof.C.cholesky]
___compcert_va_int32 [in LAProof.C.cholesky]
___compcert_va_float64 [in LAProof.C.cholesky]
___compcert_va_composite [in LAProof.C.cholesky]
___compcert_i64_utof [in LAProof.C.cholesky]
___compcert_i64_utod [in LAProof.C.cholesky]
___compcert_i64_umulh [in LAProof.C.cholesky]
___compcert_i64_umod [in LAProof.C.cholesky]
___compcert_i64_udiv [in LAProof.C.cholesky]
___compcert_i64_stof [in LAProof.C.cholesky]
___compcert_i64_stod [in LAProof.C.cholesky]
___compcert_i64_smulh [in LAProof.C.cholesky]
___compcert_i64_smod [in LAProof.C.cholesky]
___compcert_i64_shr [in LAProof.C.cholesky]
___compcert_i64_shl [in LAProof.C.cholesky]
___compcert_i64_sdiv [in LAProof.C.cholesky]
___compcert_i64_sar [in LAProof.C.cholesky]
___compcert_i64_dtou [in LAProof.C.cholesky]
___compcert_i64_dtos [in LAProof.C.cholesky]
___builtin_va_start [in LAProof.C.cholesky]
___builtin_va_end [in LAProof.C.cholesky]
___builtin_va_copy [in LAProof.C.cholesky]
___builtin_va_arg [in LAProof.C.cholesky]
___builtin_unreachable [in LAProof.C.cholesky]
___builtin_sqrt [in LAProof.C.cholesky]
___builtin_sel [in LAProof.C.cholesky]
___builtin_memcpy_aligned [in LAProof.C.cholesky]
___builtin_membar [in LAProof.C.cholesky]
___builtin_fsqrt [in LAProof.C.cholesky]
___builtin_fnmsub [in LAProof.C.cholesky]
___builtin_fnmadd [in LAProof.C.cholesky]
___builtin_fmsub [in LAProof.C.cholesky]
___builtin_fmin [in LAProof.C.cholesky]
___builtin_fmax [in LAProof.C.cholesky]
___builtin_fmadd [in LAProof.C.cholesky]
___builtin_fabsf [in LAProof.C.cholesky]
___builtin_fabs [in LAProof.C.cholesky]
___builtin_expect [in LAProof.C.cholesky]
___builtin_debug [in LAProof.C.cholesky]
___builtin_ctzll [in LAProof.C.cholesky]
___builtin_ctzl [in LAProof.C.cholesky]
___builtin_ctz [in LAProof.C.cholesky]
___builtin_clzll [in LAProof.C.cholesky]
___builtin_clzl [in LAProof.C.cholesky]
___builtin_clz [in LAProof.C.cholesky]
___builtin_clsll [in LAProof.C.cholesky]
___builtin_clsl [in LAProof.C.cholesky]
___builtin_cls [in LAProof.C.cholesky]
___builtin_bswap64 [in LAProof.C.cholesky]
___builtin_bswap32 [in LAProof.C.cholesky]
___builtin_bswap16 [in LAProof.C.cholesky]
___builtin_bswap [in LAProof.C.cholesky]
___builtin_annot_intval [in LAProof.C.cholesky]
___builtin_annot [in LAProof.C.cholesky]
_R [in LAProof.C.cholesky]
_A [in LAProof.C.cholesky]
_t'9 [in LAProof.C.bandmat]
_t'8 [in LAProof.C.bandmat]
_t'7 [in LAProof.C.bandmat]
_t'6 [in LAProof.C.bandmat]
_t'5 [in LAProof.C.bandmat]
_t'4 [in LAProof.C.bandmat]
_t'3 [in LAProof.C.bandmat]
_t'2 [in LAProof.C.bandmat]
_t'1 [in LAProof.C.bandmat]
_yi [in LAProof.C.bandmat]
_x [in LAProof.C.bandmat]
_vm [in LAProof.C.bandmat]
_surely_malloc [in LAProof.C.bandmat]
_sqrt [in LAProof.C.bandmat]
_rows [in LAProof.C.bandmat]
_printf [in LAProof.C.bandmat]
_n [in LAProof.C.bandmat]
_memset [in LAProof.C.bandmat]
_main [in LAProof.C.bandmat]
_m [in LAProof.C.bandmat]
_k [in LAProof.C.bandmat]
_j__1 [in LAProof.C.bandmat]
_j [in LAProof.C.bandmat]
_i__1 [in LAProof.C.bandmat]
_i [in LAProof.C.bandmat]
_free [in LAProof.C.bandmat]
_dm [in LAProof.C.bandmat]
_dj [in LAProof.C.bandmat]
_densemat_t [in LAProof.C.bandmat]
_densemat_get [in LAProof.C.bandmat]
_dense_to_band [in LAProof.C.bandmat]
_data_norm2 [in LAProof.C.bandmat]
_data_norm [in LAProof.C.bandmat]
_data [in LAProof.C.bandmat]
_d [in LAProof.C.bandmat]
_bw [in LAProof.C.bandmat]
_bi [in LAProof.C.bandmat]
_bandmatn_set [in LAProof.C.bandmat]
_bandmatn_get [in LAProof.C.bandmat]
_bandmatn_clear [in LAProof.C.bandmat]
_bandmatn_addto [in LAProof.C.bandmat]
_bandmat_t [in LAProof.C.bandmat]
_bandmat_solve [in LAProof.C.bandmat]
_bandmat_set [in LAProof.C.bandmat]
_bandmat_print [in LAProof.C.bandmat]
_bandmat_norm2 [in LAProof.C.bandmat]
_bandmat_norm [in LAProof.C.bandmat]
_bandmat_malloc [in LAProof.C.bandmat]
_bandmat_get [in LAProof.C.bandmat]
_bandmat_free [in LAProof.C.bandmat]
_bandmat_factor [in LAProof.C.bandmat]
_bandmat_clear [in LAProof.C.bandmat]
_bandmat_addto [in LAProof.C.bandmat]
_b [in LAProof.C.bandmat]
_abort [in LAProof.C.bandmat]
___stringlit_5 [in LAProof.C.bandmat]
___stringlit_4 [in LAProof.C.bandmat]
___stringlit_3 [in LAProof.C.bandmat]
___stringlit_2 [in LAProof.C.bandmat]
___stringlit_1 [in LAProof.C.bandmat]
___compcert_va_int64 [in LAProof.C.bandmat]
___compcert_va_int32 [in LAProof.C.bandmat]
___compcert_va_float64 [in LAProof.C.bandmat]
___compcert_va_composite [in LAProof.C.bandmat]
___compcert_i64_utof [in LAProof.C.bandmat]
___compcert_i64_utod [in LAProof.C.bandmat]
___compcert_i64_umulh [in LAProof.C.bandmat]
___compcert_i64_umod [in LAProof.C.bandmat]
___compcert_i64_udiv [in LAProof.C.bandmat]
___compcert_i64_stof [in LAProof.C.bandmat]
___compcert_i64_stod [in LAProof.C.bandmat]
___compcert_i64_smulh [in LAProof.C.bandmat]
___compcert_i64_smod [in LAProof.C.bandmat]
___compcert_i64_shr [in LAProof.C.bandmat]
___compcert_i64_shl [in LAProof.C.bandmat]
___compcert_i64_sdiv [in LAProof.C.bandmat]
___compcert_i64_sar [in LAProof.C.bandmat]
___compcert_i64_dtou [in LAProof.C.bandmat]
___compcert_i64_dtos [in LAProof.C.bandmat]
___builtin_va_start [in LAProof.C.bandmat]
___builtin_va_end [in LAProof.C.bandmat]
___builtin_va_copy [in LAProof.C.bandmat]
___builtin_va_arg [in LAProof.C.bandmat]
___builtin_unreachable [in LAProof.C.bandmat]
___builtin_sqrt [in LAProof.C.bandmat]
___builtin_sel [in LAProof.C.bandmat]
___builtin_memcpy_aligned [in LAProof.C.bandmat]
___builtin_membar [in LAProof.C.bandmat]
___builtin_fsqrt [in LAProof.C.bandmat]
___builtin_fnmsub [in LAProof.C.bandmat]
___builtin_fnmadd [in LAProof.C.bandmat]
___builtin_fmsub [in LAProof.C.bandmat]
___builtin_fmin [in LAProof.C.bandmat]
___builtin_fmax [in LAProof.C.bandmat]
___builtin_fmadd [in LAProof.C.bandmat]
___builtin_fabsf [in LAProof.C.bandmat]
___builtin_fabs [in LAProof.C.bandmat]
___builtin_expect [in LAProof.C.bandmat]
___builtin_debug [in LAProof.C.bandmat]
___builtin_ctzll [in LAProof.C.bandmat]
___builtin_ctzl [in LAProof.C.bandmat]
___builtin_ctz [in LAProof.C.bandmat]
___builtin_clzll [in LAProof.C.bandmat]
___builtin_clzl [in LAProof.C.bandmat]
___builtin_clz [in LAProof.C.bandmat]
___builtin_clsll [in LAProof.C.bandmat]
___builtin_clsl [in LAProof.C.bandmat]
___builtin_cls [in LAProof.C.bandmat]
___builtin_bswap64 [in LAProof.C.bandmat]
___builtin_bswap32 [in LAProof.C.bandmat]
___builtin_bswap16 [in LAProof.C.bandmat]
___builtin_bswap [in LAProof.C.bandmat]
___builtin_annot_intval [in LAProof.C.bandmat]
___builtin_annot [in LAProof.C.bandmat]
_PR [in LAProof.C.bandmat]
_PA [in LAProof.C.bandmat]
_P [in LAProof.C.bandmat]
_A [in LAProof.C.bandmat]
_t'1 [in LAProof.C.alloc]
_surely_malloc [in LAProof.C.alloc]
_p [in LAProof.C.alloc]
_n [in LAProof.C.alloc]
_malloc [in LAProof.C.alloc]
_main [in LAProof.C.alloc]
_int_calloc [in LAProof.C.alloc]
_i [in LAProof.C.alloc]
_free [in LAProof.C.alloc]
_exit [in LAProof.C.alloc]
_double_clear [in LAProof.C.alloc]
_double_calloc [in LAProof.C.alloc]
___compcert_va_int64 [in LAProof.C.alloc]
___compcert_va_int32 [in LAProof.C.alloc]
___compcert_va_float64 [in LAProof.C.alloc]
___compcert_va_composite [in LAProof.C.alloc]
___compcert_i64_utof [in LAProof.C.alloc]
___compcert_i64_utod [in LAProof.C.alloc]
___compcert_i64_umulh [in LAProof.C.alloc]
___compcert_i64_umod [in LAProof.C.alloc]
___compcert_i64_udiv [in LAProof.C.alloc]
___compcert_i64_stof [in LAProof.C.alloc]
___compcert_i64_stod [in LAProof.C.alloc]
___compcert_i64_smulh [in LAProof.C.alloc]
___compcert_i64_smod [in LAProof.C.alloc]
___compcert_i64_shr [in LAProof.C.alloc]
___compcert_i64_shl [in LAProof.C.alloc]
___compcert_i64_sdiv [in LAProof.C.alloc]
___compcert_i64_sar [in LAProof.C.alloc]
___compcert_i64_dtou [in LAProof.C.alloc]
___compcert_i64_dtos [in LAProof.C.alloc]
___builtin_va_start [in LAProof.C.alloc]
___builtin_va_end [in LAProof.C.alloc]
___builtin_va_copy [in LAProof.C.alloc]
___builtin_va_arg [in LAProof.C.alloc]
___builtin_unreachable [in LAProof.C.alloc]
___builtin_sqrt [in LAProof.C.alloc]
___builtin_sel [in LAProof.C.alloc]
___builtin_memcpy_aligned [in LAProof.C.alloc]
___builtin_membar [in LAProof.C.alloc]
___builtin_fsqrt [in LAProof.C.alloc]
___builtin_fnmsub [in LAProof.C.alloc]
___builtin_fnmadd [in LAProof.C.alloc]
___builtin_fmsub [in LAProof.C.alloc]
___builtin_fmin [in LAProof.C.alloc]
___builtin_fmax [in LAProof.C.alloc]
___builtin_fmadd [in LAProof.C.alloc]
___builtin_fabsf [in LAProof.C.alloc]
___builtin_fabs [in LAProof.C.alloc]
___builtin_expect [in LAProof.C.alloc]
___builtin_debug [in LAProof.C.alloc]
___builtin_ctzll [in LAProof.C.alloc]
___builtin_ctzl [in LAProof.C.alloc]
___builtin_ctz [in LAProof.C.alloc]
___builtin_clzll [in LAProof.C.alloc]
___builtin_clzl [in LAProof.C.alloc]
___builtin_clz [in LAProof.C.alloc]
___builtin_clsll [in LAProof.C.alloc]
___builtin_clsl [in LAProof.C.alloc]
___builtin_cls [in LAProof.C.alloc]
___builtin_bswap64 [in LAProof.C.alloc]
___builtin_bswap32 [in LAProof.C.alloc]
___builtin_bswap16 [in LAProof.C.alloc]
___builtin_bswap [in LAProof.C.alloc]
___builtin_annot_intval [in LAProof.C.alloc]
___builtin_annot [in LAProof.C.alloc]
| 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 | (1493 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 | (7 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 | (116 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 | (37 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 | (335 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 | (1 entry) |
| 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 | (25 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 | (10 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 | (27 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 | (9 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 | (84 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 | (842 entries) |
This page has been generated by coqdoc