| 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 | (1974 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 | (10 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 | (126 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 | (43 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 | (469 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 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) |
| 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 | (15 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 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 | (32 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 | (14 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 | (87 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 | (1118 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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]
add_to_coo_matrix_spec [definition, in LAProof.C.spec_sparse]
add_to_coo [definition, in LAProof.C.spec_sparse]
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]
AlternatePresentations [module, in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_alt_original [lemma, in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_jik_original [lemma, in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_original [definition, in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_listpairs [definition, in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_alt [definition, in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_ffuns_ffuns' [lemma, in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_ffuns [definition, in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_ffuns' [definition, in LAProof.C.matrix_model]
AlternatePresentations.WithNaN [section, in LAProof.C.matrix_model]
AlternatePresentations.WithNaN.NAN [variable, in LAProof.C.matrix_model]
AlternatePresentations.WithNaN.t [variable, in LAProof.C.matrix_model]
B
backward_subst_UT [lemma, in LAProof.accuracy_proofs.solve_model]backward_subst [definition, in LAProof.accuracy_proofs.solve_model]
backward_subst_step [definition, in LAProof.accuracy_proofs.solve_model]
bandmat [library]
BDIV_finite_e [lemma, in LAProof.accuracy_proofs.libvalidsdp]
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]
BFREXP [definition, in LAProof.accuracy_proofs.solve_model]
BFREXP_finite_strict_e [lemma, in LAProof.accuracy_proofs.solve_model]
BFREXP_finite_e [lemma, in LAProof.accuracy_proofs.solve_model]
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.common]
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]
BMULT_finite_strict_e [lemma, in LAProof.accuracy_proofs.solve_model]
Bmult_R0 [lemma, in LAProof.accuracy_proofs.solve_model]
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_coo_to_csr_matrix [lemma, in LAProof.C.verif_build_csr]
body_coo_count [lemma, in LAProof.C.verif_build_csr]
body_densematn_cfactor_and_solve [lemma, in LAProof.C.verif_densemat_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_csr_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_cholesky [lemma, in LAProof.C.verif_cholesky]
body_csr_matrix_vector_multiply_byrows [lemma, in LAProof.C.verif_sparse_byrows]
body_csr_row_vector_multiply [lemma, in LAProof.C.verif_sparse_byrows]
body_csr_matrix_rows [lemma, in LAProof.C.verif_sparse_byrows]
BoolOrder [record, in LAProof.C.distinct]
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.common]
BPLUS_neg_zero [lemma, in LAProof.accuracy_proofs.common]
BPLUS_B2R_zero [lemma, in LAProof.accuracy_proofs.libvalidsdp]
BPO [module, in LAProof.C.distinct]
bpow_fprec_lb [lemma, in LAProof.accuracy_proofs.fma_is_finite]
bpow_femax_lb [lemma, in LAProof.accuracy_proofs.fma_is_finite]
BPO_eqv_iff [lemma, in LAProof.C.partial_csr]
BPO.BO [projection, in LAProof.C.distinct]
BPO.BoolPreOrder [record, in LAProof.C.distinct]
BPO.Eqv [projection, in LAProof.C.distinct]
BPO.eqv [projection, in LAProof.C.distinct]
BPO.eqvb [projection, in LAProof.C.distinct]
BPO.eqvbspec [projection, in LAProof.C.distinct]
BPO.lt [projection, in LAProof.C.distinct]
BPO.ltb [projection, in LAProof.C.distinct]
BPO.ltb_spec [projection, in LAProof.C.distinct]
BPO.mkEqv [lemma, in LAProof.C.distinct]
BPO.mktesteqvspec [lemma, in LAProof.C.distinct]
BPO.mkteststrictspec [lemma, in LAProof.C.distinct]
BPO.PO [projection, in LAProof.C.distinct]
BPO.Strict [projection, in LAProof.C.distinct]
BPO.StrictOrderstrict [lemma, in LAProof.C.distinct]
BSQRT_nonneg [lemma, in LAProof.accuracy_proofs.libvalidsdp]
BSQRT_finite_e [lemma, in LAProof.accuracy_proofs.libvalidsdp]
BSQRT_finite_e [lemma, in LAProof.accuracy_proofs.solve_model]
bSUM [lemma, in LAProof.accuracy_proofs.sum_acc]
build_partial_CSR [constructor, in LAProof.C.partial_csr]
build_coo_csr [constructor, in LAProof.C.partial_csr]
build_csr_matrix_correct [lemma, in LAProof.C.sparse_model]
build_csr_row_correct [lemma, in LAProof.C.sparse_model]
build_csr_matrix [definition, in LAProof.C.sparse_model]
build_csr_rows [definition, in LAProof.C.sparse_model]
build_csr_row [definition, in LAProof.C.sparse_model]
build_csr_matrix_wellformed [constructor, in LAProof.C.sparse_model]
build_csr [library]
C
cd_upto [definition, in LAProof.C.partial_csr]change_composite_env_empty' [instance, in LAProof.C.densemat_lemmas]
change_composite_env_empty [instance, in LAProof.C.densemat_lemmas]
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_any [definition, in LAProof.C.matrix_model]
cholesky_jik_upto [definition, in LAProof.C.matrix_model]
cholesky_return'_e [lemma, in LAProof.C.verif_densemat_cholesky]
cholesky_return' [definition, in LAProof.C.verif_densemat_cholesky]
cholesky_jik_spec_backwards_finite [lemma, in LAProof.accuracy_proofs.libvalidsdp]
cholesky_bound [definition, in LAProof.accuracy_proofs.libvalidsdp]
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]
cholesky_return_success [lemma, in LAProof.accuracy_proofs.solve_model]
cholesky_success_R_finite [lemma, in LAProof.accuracy_proofs.solve_model]
cholesky_return [definition, in LAProof.accuracy_proofs.solve_model]
cholesky_success [definition, in LAProof.accuracy_proofs.solve_model]
cholesky_jik_upto [definition, in LAProof.accuracy_proofs.solve_model]
cholesky_jik_spec [definition, in LAProof.accuracy_proofs.solve_model]
cholesky_jik_ij [definition, in LAProof.accuracy_proofs.solve_model]
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.cholesky]
composites [definition, in LAProof.C.alloc]
composites [definition, in LAProof.C.build_csr]
composites [definition, in LAProof.C.densemat]
composites [definition, in LAProof.C.bandmat]
CompSpecs [instance, in LAProof.C.spec_densemat]
CompSpecs [instance, in LAProof.C.spec_alloc]
CompSpecs [instance, in LAProof.C.spec_sparse]
CompSpecs [instance, in LAProof.C.verif_cholesky]
CoordBO [instance, in LAProof.C.sparse_model]
CoordBPO [instance, in LAProof.C.sparse_model]
CoordPO [instance, in LAProof.C.sparse_model]
coord_sorted_e [lemma, in LAProof.C.partial_csr]
coord_leb [definition, in LAProof.C.sparse_model]
coord_le [definition, in LAProof.C.sparse_model]
coord_eqb [definition, in LAProof.C.sparse_model]
coo_less_spec [definition, in LAProof.C.spec_sparse]
coo_count_spec [definition, in LAProof.C.spec_sparse]
coo_quicksort_spec [definition, in LAProof.C.spec_sparse]
coo_to_csr_matrix_spec [definition, in LAProof.C.spec_sparse]
coo_rep [definition, in LAProof.C.spec_sparse]
coo_to_matrix_build_csr_matrix [lemma, in LAProof.C.partial_csr]
coo_upto_wellformed [lemma, in LAProof.C.partial_csr]
coo_csr_sind [definition, in LAProof.C.partial_csr]
coo_csr_rec [definition, in LAProof.C.partial_csr]
coo_csr_ind [definition, in LAProof.C.partial_csr]
coo_csr_rect [definition, in LAProof.C.partial_csr]
coo_csr [inductive, in LAProof.C.partial_csr]
coo_upto [definition, in LAProof.C.partial_csr]
coo_entry_bounds [lemma, in LAProof.C.partial_csr]
coo_matrix_equiv_trans [lemma, in LAProof.C.sparse_model]
coo_matrix_equiv_symm [lemma, in LAProof.C.sparse_model]
coo_matrix_equiv_refl [lemma, in LAProof.C.sparse_model]
coo_to_matrix_equiv [lemma, in LAProof.C.sparse_model]
coo_to_matrix [definition, in LAProof.C.sparse_model]
coo_matrix_wellformed_equiv [lemma, in LAProof.C.sparse_model]
coo_matrix_equiv [definition, in LAProof.C.sparse_model]
coo_matrix_wellformed [definition, in LAProof.C.sparse_model]
coo_entries [projection, in LAProof.C.sparse_model]
coo_cols [projection, in LAProof.C.sparse_model]
coo_rows [projection, in LAProof.C.sparse_model]
coo_matrix [record, in LAProof.C.sparse_model]
count_distinct_range_same [lemma, in LAProof.C.distinct]
count_distinct_1 [lemma, in LAProof.C.distinct]
count_distinct_aux_lemma [lemma, in LAProof.C.distinct]
count_distinct_aux_mono [lemma, in LAProof.C.distinct]
count_distinct_noincr [lemma, in LAProof.C.distinct]
count_distinct_incr' [lemma, in LAProof.C.distinct]
count_distinct_incr [lemma, in LAProof.C.distinct]
count_distinct_mono [lemma, in LAProof.C.distinct]
count_distinct_bound' [lemma, in LAProof.C.distinct]
count_distinct_bound [lemma, in LAProof.C.distinct]
count_distinct [definition, in LAProof.C.distinct]
count_distinct_aux [definition, in LAProof.C.distinct]
crazy [definition, in LAProof.accuracy_proofs.mv_mathcomp]
create_coo_matrix_spec [definition, in LAProof.C.spec_sparse]
csr_matrix_vector_multiply_spec [definition, in LAProof.C.spec_sparse]
csr_matrix_vector_multiply_byrows_spec [definition, in LAProof.C.spec_sparse]
csr_row_vector_multiply_spec [definition, in LAProof.C.spec_sparse]
csr_matrix_rows_spec [definition, in LAProof.C.spec_sparse]
csr_token [definition, in LAProof.C.spec_sparse]
csr_token' [definition, in LAProof.C.spec_sparse]
csr_rep [definition, in LAProof.C.spec_sparse]
csr_rep' [definition, in LAProof.C.spec_sparse]
csr_row_rep_colsnonneg [lemma, in LAProof.C.partial_csr]
csr_multiply_loop_body [lemma, in LAProof.C.verif_sparse]
csr_matrix_wellformed_sind [definition, in LAProof.C.sparse_model]
csr_matrix_wellformed_rec [definition, in LAProof.C.sparse_model]
csr_matrix_wellformed_ind [definition, in LAProof.C.sparse_model]
csr_matrix_wellformed_rect [definition, in LAProof.C.sparse_model]
csr_matrix_wellformed [inductive, in LAProof.C.sparse_model]
csr_row_rep_property [lemma, in LAProof.C.sparse_model]
csr_row_rep_col_range [lemma, in LAProof.C.sparse_model]
csr_row_rep_cols_nonneg [lemma, in LAProof.C.sparse_model]
csr_to_matrix_cols [lemma, in LAProof.C.sparse_model]
csr_to_matrix_rows [lemma, in LAProof.C.sparse_model]
csr_to_matrix [definition, in LAProof.C.sparse_model]
csr_row_rep_sind [definition, in LAProof.C.sparse_model]
csr_row_rep_ind [definition, in LAProof.C.sparse_model]
csr_row_rep_val [constructor, in LAProof.C.sparse_model]
csr_row_rep_zero [constructor, in LAProof.C.sparse_model]
csr_row_rep_nil [constructor, in LAProof.C.sparse_model]
csr_row_rep [inductive, in LAProof.C.sparse_model]
csr_rows [projection, in LAProof.C.sparse_model]
csr_row_ptr [projection, in LAProof.C.sparse_model]
csr_col_ind [projection, in LAProof.C.sparse_model]
csr_vals [projection, in LAProof.C.sparse_model]
csr_cols [projection, in LAProof.C.sparse_model]
csr_matrix [record, in LAProof.C.sparse_model]
ctype_of_the_type [lemma, in LAProof.C.spec_densemat]
ctype_of_type [definition, in LAProof.C.spec_densemat]
cV_of_list_of_cV [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
cV_of_list [definition, in LAProof.accuracy_proofs.mv_mathcomp]
D
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.dot_acc]
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_eq [lemma, in LAProof.accuracy_proofs.libvalidsdp]
default_abs_eq [lemma, in LAProof.accuracy_proofs.libvalidsdp]
default_abs_nonzero [lemma, in LAProof.accuracy_proofs.libvalidsdp]
default_abs [definition, in LAProof.accuracy_proofs.libvalidsdp]
default_rel [definition, in LAProof.accuracy_proofs.libvalidsdp]
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_cfactor_and_solve_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]
diag_finite_R_finite [lemma, in LAProof.accuracy_proofs.solve_model]
digits_max_mantissa [lemma, in LAProof.accuracy_proofs.libvalidsdp]
distinct [library]
done_to_n [definition, in LAProof.C.verif_cholesky]
done_to_ij [definition, in LAProof.C.verif_cholesky]
dotprod [definition, in LAProof.C.floatlib]
dotprod [definition, in LAProof.accuracy_proofs.dotprod_model]
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_mixed_error_rel [lemma, in LAProof.accuracy_proofs.dot_acc_lemmas]
dotprod_forward_error_rel [lemma, in LAProof.accuracy_proofs.dot_acc_lemmas]
dotprod_congr [lemma, in LAProof.C.floatlib]
dotprod_forward_error [lemma, in LAProof.accuracy_proofs.dot_acc]
dotprod_mixed_error [lemma, in LAProof.accuracy_proofs.dot_acc]
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_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.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]
E [abbreviation, in LAProof.accuracy_proofs.dot_acc]
entries_correspond [definition, in LAProof.C.partial_csr]
enum_mem_ordinal [lemma, in LAProof.C.matrix_model]
eps [abbreviation, in LAProof.accuracy_proofs.libvalidsdp]
eqv_cda [lemma, in LAProof.C.distinct]
eq_in_subrange [lemma, in LAProof.C.matrix_model]
eta [abbreviation, in LAProof.accuracy_proofs.libvalidsdp]
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]
F [abbreviation, in LAProof.accuracy_proofs.libvalidsdp]
Faddmx_mixed_error [lemma, in LAProof.accuracy_proofs.vec_op_acc]
fcmsum_l2r [definition, in LAProof.accuracy_proofs.libvalidsdp]
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_max [definition, in LAProof.accuracy_proofs.libvalidsdp]
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]
Fmulmx_matrix_vector_mult [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
foldl_congr [lemma, in LAProof.accuracy_proofs.common]
fold_csr_rep' [lemma, in LAProof.C.verif_build_csr]
fold_coo_rep [lemma, in LAProof.C.verif_build_csr]
fold_left_preserves [lemma, in LAProof.C.densemat_lemmas]
Forall_take_ord_enum [lemma, in LAProof.accuracy_proofs.libvalidsdp]
format_FT2R [lemma, in LAProof.accuracy_proofs.libvalidsdp]
ForwardError [section, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError [section, in LAProof.accuracy_proofs.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.fma_dot_acc]
ForwardError.Hfin [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.Hlen [variable, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.Hlen [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.NAN [variable, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.NAN [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.t [variable, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.t [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.v1 [variable, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.v1 [variable, in LAProof.accuracy_proofs.dot_acc]
ForwardError.v2 [variable, in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.v2 [variable, in LAProof.accuracy_proofs.dot_acc]
forward_subst_LT [lemma, in LAProof.accuracy_proofs.solve_model]
forward_subst [definition, in LAProof.accuracy_proofs.solve_model]
forward_subst_step [definition, in LAProof.accuracy_proofs.solve_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]
fspec [definition, in LAProof.accuracy_proofs.libvalidsdp]
fspec_eta_nonzero [lemma, in LAProof.accuracy_proofs.libvalidsdp]
fSUM [lemma, in LAProof.accuracy_proofs.sum_acc]
fsum_l2r_rec_finite_e1 [lemma, in LAProof.accuracy_proofs.libvalidsdp]
fsum_l2r_rec_finite_e [lemma, in LAProof.accuracy_proofs.libvalidsdp]
fsum_l2r_rec [definition, in LAProof.accuracy_proofs.libvalidsdp]
Fsum_forward_error [lemma, in LAProof.accuracy_proofs.sum_acc]
Fsum_backward_error [lemma, in LAProof.accuracy_proofs.sum_acc]
FS_val_ext [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fsqrt' [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fdiv' [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fdiv [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fopp' [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fopp [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fmult' [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fmult [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fplus' [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fplus [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FS_val_mkFS [lemma, in LAProof.accuracy_proofs.libvalidsdp]
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_BDIV_congr [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FT2R_feq [lemma, in LAProof.accuracy_proofs.libvalidsdp]
FT2R_congr [lemma, in LAProof.accuracy_proofs.libvalidsdp]
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_coo_to_csr_matrix [definition, in LAProof.C.sparse]
f_coo_count [definition, in LAProof.C.sparse]
f_coo_quicksort [definition, in LAProof.C.sparse]
f_coo_less [definition, in LAProof.C.sparse]
f_swap [definition, in LAProof.C.sparse]
f_add_to_coo_matrix [definition, in LAProof.C.sparse]
f_create_coo_matrix [definition, in LAProof.C.sparse]
f_csr_matrix_vector_multiply_byrows [definition, in LAProof.C.sparse]
f_csr_row_vector_multiply [definition, in LAProof.C.sparse]
f_csr_matrix_rows [definition, in LAProof.C.sparse]
f_csr_matrix_vector_multiply [definition, in LAProof.C.sparse]
f_cholesky [definition, in LAProof.C.cholesky]
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_coo_to_csr_matrix [definition, in LAProof.C.build_csr]
f_coo_count [definition, in LAProof.C.build_csr]
f_coo_quicksort [definition, in LAProof.C.build_csr]
f_coo_less [definition, in LAProof.C.build_csr]
f_swap [definition, in LAProof.C.build_csr]
f_add_to_coo_matrix [definition, in LAProof.C.build_csr]
f_create_coo_matrix [definition, in LAProof.C.build_csr]
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_densematn_cfactor_and_solve [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_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' [definition, in LAProof.accuracy_proofs.libvalidsdp]
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.FMA_mulmx_fma_dotprod [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
F.FMA_mulmx_col [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
F.FMA_mulmx_row [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
F.FMA_mulmx [definition, in LAProof.accuracy_proofs.mv_mathcomp]
F.FMA_dotprod [definition, 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_col [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.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.vec_op_acc]
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.sum_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.cholesky]
global_definitions [definition, in LAProof.C.alloc]
global_definitions [definition, in LAProof.C.build_csr]
global_definitions [definition, in LAProof.C.densemat]
global_definitions [definition, in LAProof.C.bandmat]
Gprog [definition, in LAProof.C.spec_sparse]
Gprog [definition, in LAProof.C.verif_alloc]
Gprog [definition, in LAProof.C.verif_cholesky]
Gprog [definition, in LAProof.C.densemat_lemmas]
g_pos [lemma, in LAProof.accuracy_proofs.common]
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.gemm_acc]
g1 [abbreviation, in LAProof.accuracy_proofs.dot_acc]
g1 [abbreviation, in LAProof.accuracy_proofs.dot_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.cholesky]
Info [module, in LAProof.C.alloc]
Info [module, in LAProof.C.build_csr]
Info [module, in LAProof.C.densemat]
Info [module, in LAProof.C.bandmat]
Info.abi [definition, in LAProof.C.sparse]
Info.abi [definition, in LAProof.C.cholesky]
Info.abi [definition, in LAProof.C.alloc]
Info.abi [definition, in LAProof.C.build_csr]
Info.abi [definition, in LAProof.C.densemat]
Info.abi [definition, in LAProof.C.bandmat]
Info.arch [definition, in LAProof.C.sparse]
Info.arch [definition, in LAProof.C.cholesky]
Info.arch [definition, in LAProof.C.alloc]
Info.arch [definition, in LAProof.C.build_csr]
Info.arch [definition, in LAProof.C.densemat]
Info.arch [definition, in LAProof.C.bandmat]
Info.big_endian [definition, in LAProof.C.sparse]
Info.big_endian [definition, in LAProof.C.cholesky]
Info.big_endian [definition, in LAProof.C.alloc]
Info.big_endian [definition, in LAProof.C.build_csr]
Info.big_endian [definition, in LAProof.C.densemat]
Info.big_endian [definition, in LAProof.C.bandmat]
Info.bitsize [definition, in LAProof.C.sparse]
Info.bitsize [definition, in LAProof.C.cholesky]
Info.bitsize [definition, in LAProof.C.alloc]
Info.bitsize [definition, in LAProof.C.build_csr]
Info.bitsize [definition, in LAProof.C.densemat]
Info.bitsize [definition, in LAProof.C.bandmat]
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.cholesky]
Info.build_tag [definition, in LAProof.C.cholesky]
Info.build_number [definition, in LAProof.C.cholesky]
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.build_branch [definition, in LAProof.C.build_csr]
Info.build_tag [definition, in LAProof.C.build_csr]
Info.build_number [definition, in LAProof.C.build_csr]
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.bandmat]
Info.build_tag [definition, in LAProof.C.bandmat]
Info.build_number [definition, in LAProof.C.bandmat]
Info.model [definition, in LAProof.C.sparse]
Info.model [definition, in LAProof.C.cholesky]
Info.model [definition, in LAProof.C.alloc]
Info.model [definition, in LAProof.C.build_csr]
Info.model [definition, in LAProof.C.densemat]
Info.model [definition, in LAProof.C.bandmat]
Info.normalized [definition, in LAProof.C.sparse]
Info.normalized [definition, in LAProof.C.cholesky]
Info.normalized [definition, in LAProof.C.alloc]
Info.normalized [definition, in LAProof.C.build_csr]
Info.normalized [definition, in LAProof.C.densemat]
Info.normalized [definition, in LAProof.C.bandmat]
Info.source_file [definition, in LAProof.C.sparse]
Info.source_file [definition, in LAProof.C.cholesky]
Info.source_file [definition, in LAProof.C.alloc]
Info.source_file [definition, in LAProof.C.build_csr]
Info.source_file [definition, in LAProof.C.densemat]
Info.source_file [definition, in LAProof.C.bandmat]
Info.version [definition, in LAProof.C.sparse]
Info.version [definition, in LAProof.C.cholesky]
Info.version [definition, in LAProof.C.alloc]
Info.version [definition, in LAProof.C.build_csr]
Info.version [definition, in LAProof.C.densemat]
Info.version [definition, in LAProof.C.bandmat]
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]
iszero [definition, in LAProof.accuracy_proofs.libvalidsdp]
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
last_R_finite [lemma, in LAProof.accuracy_proofs.solve_model]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]
le1_sorted [lemma, in LAProof.C.distinct]
libvalidsdp [library]
listlist_of_mx_inj [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
listlist_of_mx_col_mx [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
listlist_of_mx_of_listlist [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
listlist_of_mx [definition, in LAProof.accuracy_proofs.mv_mathcomp]
lists_of_fun [definition, in LAProof.C.verif_cholesky]
list_of_cV_col_mx [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
list_dotprod [definition, in LAProof.accuracy_proofs.mv_mathcomp]
list_of_cV_of_list [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
list_of_cV [definition, in LAProof.accuracy_proofs.mv_mathcomp]
list_of_fun [definition, in LAProof.C.verif_cholesky]
lshift1 [definition, in LAProof.C.matrix_model]
LVDSP_cholesky_success [lemma, in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_cholesky_spec [lemma, in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_lemma_2_1 [lemma, in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_ytildes_eq [lemma, in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_ytilded_eq [lemma, in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_stilde_eq [lemma, in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_fcmsum_eq [lemma, in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_NAN [definition, in LAProof.accuracy_proofs.libvalidsdp]
M
Malloc [instance, in LAProof.C.spec_alloc]map_inj [lemma, in LAProof.C.matrix_model]
map_const_len [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
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.floatlib]
matrix [definition, in LAProof.C.verif_cholesky]
matrix_vector_mult [definition, in LAProof.accuracy_proofs.mv_mathcomp]
matrix_cols_listlist_of_mx [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
matrix_rows_listlist_of_mx [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
matrix_cols_nat [definition, in LAProof.accuracy_proofs.mv_mathcomp]
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_index_Z [lemma, in LAProof.C.partial_csr]
matrix_upd [definition, in LAProof.C.partial_csr]
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]
max_mantissa_bounded [lemma, in LAProof.accuracy_proofs.libvalidsdp]
max_mantissa [definition, in LAProof.accuracy_proofs.libvalidsdp]
MINUS_PLUS_BOPP [lemma, in LAProof.accuracy_proofs.common]
mirror_UT [definition, in LAProof.C.matrix_model]
MixedError [section, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError [section, in LAProof.accuracy_proofs.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.fma_dot_acc]
MixedError.Hfin [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.Hlen [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.Hlen [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.NAN [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.NAN [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.t [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.t [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.v1 [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.v1 [variable, in LAProof.accuracy_proofs.dot_acc]
MixedError.v2 [variable, in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.v2 [variable, in LAProof.accuracy_proofs.dot_acc]
mkFS [definition, in LAProof.accuracy_proofs.libvalidsdp]
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]
mx_of_listlist_of_mx [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
mx_of_listlist [definition, in LAProof.accuracy_proofs.mv_mathcomp]
N
n [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]n [abbreviation, in LAProof.accuracy_proofs.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_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 [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.dot_acc]
neg_zero [definition, in LAProof.C.verif_cholesky]
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.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 [abbreviation, in LAProof.accuracy_proofs.dot_acc]
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]
no_extra_zeros [definition, in LAProof.C.partial_csr]
nth_ord_enum' [lemma, in LAProof.C.matrix_model]
nth_list_of_cV [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
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]
ord_enum_S [lemma, in LAProof.accuracy_proofs.libvalidsdp]
origFIS [definition, in LAProof.accuracy_proofs.libvalidsdp]
P
partial_CSR_VAL_defined [lemma, in LAProof.C.partial_csr]partial_CSR_properties [lemma, in LAProof.C.partial_csr]
partial_CSR_lastrows [lemma, in LAProof.C.partial_csr]
partial_CSR_newrow [lemma, in LAProof.C.partial_csr]
partial_CSR_skiprow [lemma, in LAProof.C.partial_csr]
partial_CSR_0 [lemma, in LAProof.C.partial_csr]
partial_CSR_newcol [lemma, in LAProof.C.partial_csr]
partial_CSR_duplicate [lemma, in LAProof.C.partial_csr]
partial_CSR_rowptr' [lemma, in LAProof.C.partial_csr]
partial_CSR_sind [definition, in LAProof.C.partial_csr]
partial_CSR_ind [definition, in LAProof.C.partial_csr]
partial_CSR [inductive, in LAProof.C.partial_csr]
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]
partial_csr [library]
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]
prec_lt_emax [lemma, in LAProof.accuracy_proofs.libvalidsdp]
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.cholesky]
prog [definition, in LAProof.C.alloc]
prog [definition, in LAProof.C.build_csr]
prog [definition, in LAProof.C.densemat]
prog [definition, in LAProof.C.bandmat]
public_idents [definition, in LAProof.C.sparse]
public_idents [definition, in LAProof.C.cholesky]
public_idents [definition, in LAProof.C.alloc]
public_idents [definition, in LAProof.C.build_csr]
public_idents [definition, in LAProof.C.densemat]
public_idents [definition, in LAProof.C.bandmat]
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]
reflect_coord_le [lemma, in LAProof.C.sparse_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]
rev_List_rev [lemma, in LAProof.accuracy_proofs.solve_model]
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]
rowptr_sorted_e1 [lemma, in LAProof.C.sparse_model]
rowptr_sorted_e [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
SBO [section, in LAProof.C.distinct]SBO.A [variable, in LAProof.C.distinct]
SBO.InhA [variable, in LAProof.C.distinct]
SBO.le [variable, in LAProof.C.distinct]
SBO.SBO [variable, in LAProof.C.distinct]
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_list_of_cV [lemma, in LAProof.accuracy_proofs.mv_mathcomp]
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]
solve_model [library]
sorted [inductive, in LAProof.C.distinct]
sorted_sublist [lemma, in LAProof.C.distinct]
sorted_e1 [lemma, in LAProof.C.distinct]
sorted_app_e3 [lemma, in LAProof.C.distinct]
sorted_app [lemma, in LAProof.C.distinct]
sorted_i [lemma, in LAProof.C.distinct]
sorted_e [lemma, in LAProof.C.distinct]
sorted_sind [definition, in LAProof.C.distinct]
sorted_ind [definition, in LAProof.C.distinct]
sorted_cons [constructor, in LAProof.C.distinct]
sorted_1 [constructor, in LAProof.C.distinct]
sorted_nil [constructor, in LAProof.C.distinct]
sorted_cons_e2 [lemma, in LAProof.C.partial_csr]
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]
SparseVSU [definition, in LAProof.C.VSU_sparse]
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_imports [definition, in LAProof.C.spec_sparse]
sparse_dotprod_forward_error [lemma, in LAProof.accuracy_proofs.dot_acc]
sparse_model [library]
spec_densemat [library]
spec_alloc [library]
spec_sparse [library]
SQRT_nonneg [lemma, in LAProof.accuracy_proofs.solve_model]
stilde [definition, in LAProof.accuracy_proofs.libvalidsdp]
stilde_subtract_loop [lemma, in LAProof.accuracy_proofs.libvalidsdp]
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]
subtractoff_spec [definition, in LAProof.C.spec_densemat]
subtract_another [lemma, in LAProof.C.matrix_model]
subtract_loop_any [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_another [lemma, in LAProof.C.verif_cholesky]
subtract_loop [definition, in LAProof.C.verif_cholesky]
subtract_loop_finite_e [lemma, in LAProof.accuracy_proofs.solve_model]
subtract_loop_jik [definition, in LAProof.accuracy_proofs.solve_model]
subtract_loop [definition, in LAProof.accuracy_proofs.solve_model]
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_any_accuracy [lemma, in LAProof.C.sparse_model]
sum_any_sind [definition, in LAProof.C.sparse_model]
sum_any_ind [definition, in LAProof.C.sparse_model]
Sum_Any_perm [constructor, in LAProof.C.sparse_model]
Sum_Any_split [constructor, in LAProof.C.sparse_model]
Sum_Any_1 [constructor, in LAProof.C.sparse_model]
Sum_Any_0 [constructor, in LAProof.C.sparse_model]
sum_any [inductive, in LAProof.C.sparse_model]
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]
swap_spec [definition, in LAProof.C.spec_sparse]
T
take_snoc [lemma, in LAProof.C.matrix_model]take_ord_enum [lemma, in LAProof.C.matrix_model]
take_sublist [lemma, in LAProof.C.densemat_lemmas]
test [projection, in LAProof.C.distinct]
test_spec [projection, in LAProof.C.distinct]
the_type [definition, in LAProof.C.spec_densemat]
the_ctype [definition, in LAProof.C.spec_densemat]
the_loop_body [definition, in LAProof.C.verif_sparse]
the_FIS [definition, in LAProof.accuracy_proofs.libvalidsdp]
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_coo [definition, in LAProof.C.spec_sparse]
t_csr [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_i_lt_j [lemma, in LAProof.C.verif_cholesky]
update_mx [definition, in LAProof.accuracy_proofs.solve_model]
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]
verif_build_csr [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.spec_sparse]
Vprog [definition, in LAProof.C.verif_cholesky]
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.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.dot_acc]
v1R [abbreviation, in LAProof.accuracy_proofs.dotprod_model]
v1R' [abbreviation, in LAProof.accuracy_proofs.fma_dot_acc]
v1R' [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]
v2R' [abbreviation, in LAProof.accuracy_proofs.dot_acc]
W
widen_ik [definition, in LAProof.C.matrix_model]WithNaN [section, in LAProof.accuracy_proofs.libvalidsdp]
WithNan [section, in LAProof.accuracy_proofs.sum_acc]
WithNaN [section, in LAProof.accuracy_proofs.solve_model]
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.A [section, in LAProof.accuracy_proofs.libvalidsdp]
WithNaN.NAN [variable, in LAProof.accuracy_proofs.libvalidsdp]
WithNan.NAN [variable, in LAProof.accuracy_proofs.sum_acc]
WithNaN.NAN [variable, in LAProof.accuracy_proofs.solve_model]
WithNAN.NAN [variable, in LAProof.accuracy_proofs.gemv_acc]
WithNaN.t [variable, in LAProof.accuracy_proofs.libvalidsdp]
WithNan.t [variable, in LAProof.accuracy_proofs.sum_acc]
WithNaN.t [variable, in LAProof.accuracy_proofs.solve_model]
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]
Y
ytilded [definition, in LAProof.accuracy_proofs.libvalidsdp]ytilded_subtract_loop [lemma, in LAProof.accuracy_proofs.libvalidsdp]
ytildes [definition, in LAProof.accuracy_proofs.libvalidsdp]
ytildes_subtract_loop [lemma, in LAProof.accuracy_proofs.libvalidsdp]
Z
Zcholesky_return [definition, in LAProof.accuracy_proofs.solve_model]zerof [instance, in LAProof.C.matrix_model]
zerof [instance, in LAProof.C.floatlib]
Zlength_seq [lemma, in LAProof.C.floatlib]
Zlength_iota [lemma, in LAProof.C.verif_cholesky]
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_vector_sub [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_column_major [lemma, in LAProof.C.densemat_lemmas]
Znth_ord_enum [lemma, in LAProof.C.densemat_lemmas]
_
_t'9 [definition, in LAProof.C.sparse]_t'8 [definition, in LAProof.C.sparse]
_t'7 [definition, in LAProof.C.sparse]
_t'6 [definition, in LAProof.C.sparse]
_t'5 [definition, in LAProof.C.sparse]
_t'4 [definition, in LAProof.C.sparse]
_t'3 [definition, in LAProof.C.sparse]
_t'2 [definition, in LAProof.C.sparse]
_t'15 [definition, in LAProof.C.sparse]
_t'14 [definition, in LAProof.C.sparse]
_t'13 [definition, in LAProof.C.sparse]
_t'12 [definition, in LAProof.C.sparse]
_t'11 [definition, in LAProof.C.sparse]
_t'10 [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]
_swap [definition, in LAProof.C.sparse]
_surely_malloc [definition, in LAProof.C.sparse]
_s [definition, in LAProof.C.sparse]
_rows [definition, in LAProof.C.sparse]
_row_ptr [definition, in LAProof.C.sparse]
_row_ind [definition, in LAProof.C.sparse]
_right [definition, in LAProof.C.sparse]
_ri [definition, in LAProof.C.sparse]
_rb [definition, in LAProof.C.sparse]
_ra [definition, in LAProof.C.sparse]
_r [definition, in LAProof.C.sparse]
_q [definition, in LAProof.C.sparse]
_pval [definition, in LAProof.C.sparse]
_prow_ind [definition, in LAProof.C.sparse]
_pcol_ind [definition, in LAProof.C.sparse]
_p [definition, in LAProof.C.sparse]
_next [definition, in LAProof.C.sparse]
_n [definition, in LAProof.C.sparse]
_mid [definition, in LAProof.C.sparse]
_maxn [definition, in LAProof.C.sparse]
_main [definition, in LAProof.C.sparse]
_m [definition, in LAProof.C.sparse]
_lo [definition, in LAProof.C.sparse]
_left [definition, in LAProof.C.sparse]
_l [definition, in LAProof.C.sparse]
_k [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]
_exit [definition, in LAProof.C.sparse]
_csr_row_vector_multiply [definition, in LAProof.C.sparse]
_csr_matrix_vector_multiply_byrows [definition, in LAProof.C.sparse]
_csr_matrix_vector_multiply [definition, in LAProof.C.sparse]
_csr_matrix_rows [definition, in LAProof.C.sparse]
_csr_matrix [definition, in LAProof.C.sparse]
_create_coo_matrix [definition, in LAProof.C.sparse]
_count [definition, in LAProof.C.sparse]
_coo_to_csr_matrix [definition, in LAProof.C.sparse]
_coo_quicksort [definition, in LAProof.C.sparse]
_coo_matrix [definition, in LAProof.C.sparse]
_coo_less [definition, in LAProof.C.sparse]
_coo_count [definition, in LAProof.C.sparse]
_cols [definition, in LAProof.C.sparse]
_col_ind [definition, in LAProof.C.sparse]
_ci [definition, in LAProof.C.sparse]
_c [definition, in LAProof.C.sparse]
_base [definition, in LAProof.C.sparse]
_b [definition, in LAProof.C.sparse]
_add_to_coo_matrix [definition, in LAProof.C.sparse]
_a [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'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'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]
_t'9 [definition, in LAProof.C.build_csr]
_t'8 [definition, in LAProof.C.build_csr]
_t'7 [definition, in LAProof.C.build_csr]
_t'6 [definition, in LAProof.C.build_csr]
_t'5 [definition, in LAProof.C.build_csr]
_t'4 [definition, in LAProof.C.build_csr]
_t'3 [definition, in LAProof.C.build_csr]
_t'2 [definition, in LAProof.C.build_csr]
_t'15 [definition, in LAProof.C.build_csr]
_t'14 [definition, in LAProof.C.build_csr]
_t'13 [definition, in LAProof.C.build_csr]
_t'12 [definition, in LAProof.C.build_csr]
_t'11 [definition, in LAProof.C.build_csr]
_t'10 [definition, in LAProof.C.build_csr]
_t'1 [definition, in LAProof.C.build_csr]
_x [definition, in LAProof.C.build_csr]
_val [definition, in LAProof.C.build_csr]
_swap [definition, in LAProof.C.build_csr]
_surely_malloc [definition, in LAProof.C.build_csr]
_rows [definition, in LAProof.C.build_csr]
_row_ptr [definition, in LAProof.C.build_csr]
_row_ind [definition, in LAProof.C.build_csr]
_right [definition, in LAProof.C.build_csr]
_ri [definition, in LAProof.C.build_csr]
_rb [definition, in LAProof.C.build_csr]
_ra [definition, in LAProof.C.build_csr]
_r [definition, in LAProof.C.build_csr]
_q [definition, in LAProof.C.build_csr]
_pval [definition, in LAProof.C.build_csr]
_prow_ind [definition, in LAProof.C.build_csr]
_pcol_ind [definition, in LAProof.C.build_csr]
_p [definition, in LAProof.C.build_csr]
_n [definition, in LAProof.C.build_csr]
_mid [definition, in LAProof.C.build_csr]
_maxn [definition, in LAProof.C.build_csr]
_main [definition, in LAProof.C.build_csr]
_lo [definition, in LAProof.C.build_csr]
_left [definition, in LAProof.C.build_csr]
_l [definition, in LAProof.C.build_csr]
_k [definition, in LAProof.C.build_csr]
_j [definition, in LAProof.C.build_csr]
_i [definition, in LAProof.C.build_csr]
_hi [definition, in LAProof.C.build_csr]
_exit [definition, in LAProof.C.build_csr]
_csr_matrix [definition, in LAProof.C.build_csr]
_create_coo_matrix [definition, in LAProof.C.build_csr]
_count [definition, in LAProof.C.build_csr]
_coo_to_csr_matrix [definition, in LAProof.C.build_csr]
_coo_quicksort [definition, in LAProof.C.build_csr]
_coo_matrix [definition, in LAProof.C.build_csr]
_coo_less [definition, in LAProof.C.build_csr]
_coo_count [definition, in LAProof.C.build_csr]
_cols [definition, in LAProof.C.build_csr]
_col_ind [definition, in LAProof.C.build_csr]
_ci [definition, in LAProof.C.build_csr]
_c [definition, in LAProof.C.build_csr]
_base [definition, in LAProof.C.build_csr]
_b [definition, in LAProof.C.build_csr]
_add_to_coo_matrix [definition, in LAProof.C.build_csr]
_a [definition, in LAProof.C.build_csr]
___compcert_va_int64 [definition, in LAProof.C.build_csr]
___compcert_va_int32 [definition, in LAProof.C.build_csr]
___compcert_va_float64 [definition, in LAProof.C.build_csr]
___compcert_va_composite [definition, in LAProof.C.build_csr]
___compcert_i64_utof [definition, in LAProof.C.build_csr]
___compcert_i64_utod [definition, in LAProof.C.build_csr]
___compcert_i64_umulh [definition, in LAProof.C.build_csr]
___compcert_i64_umod [definition, in LAProof.C.build_csr]
___compcert_i64_udiv [definition, in LAProof.C.build_csr]
___compcert_i64_stof [definition, in LAProof.C.build_csr]
___compcert_i64_stod [definition, in LAProof.C.build_csr]
___compcert_i64_smulh [definition, in LAProof.C.build_csr]
___compcert_i64_smod [definition, in LAProof.C.build_csr]
___compcert_i64_shr [definition, in LAProof.C.build_csr]
___compcert_i64_shl [definition, in LAProof.C.build_csr]
___compcert_i64_sdiv [definition, in LAProof.C.build_csr]
___compcert_i64_sar [definition, in LAProof.C.build_csr]
___compcert_i64_dtou [definition, in LAProof.C.build_csr]
___compcert_i64_dtos [definition, in LAProof.C.build_csr]
___builtin_va_start [definition, in LAProof.C.build_csr]
___builtin_va_end [definition, in LAProof.C.build_csr]
___builtin_va_copy [definition, in LAProof.C.build_csr]
___builtin_va_arg [definition, in LAProof.C.build_csr]
___builtin_unreachable [definition, in LAProof.C.build_csr]
___builtin_sqrt [definition, in LAProof.C.build_csr]
___builtin_sel [definition, in LAProof.C.build_csr]
___builtin_memcpy_aligned [definition, in LAProof.C.build_csr]
___builtin_membar [definition, in LAProof.C.build_csr]
___builtin_fsqrt [definition, in LAProof.C.build_csr]
___builtin_fnmsub [definition, in LAProof.C.build_csr]
___builtin_fnmadd [definition, in LAProof.C.build_csr]
___builtin_fmsub [definition, in LAProof.C.build_csr]
___builtin_fmin [definition, in LAProof.C.build_csr]
___builtin_fmax [definition, in LAProof.C.build_csr]
___builtin_fmadd [definition, in LAProof.C.build_csr]
___builtin_fabsf [definition, in LAProof.C.build_csr]
___builtin_fabs [definition, in LAProof.C.build_csr]
___builtin_expect [definition, in LAProof.C.build_csr]
___builtin_debug [definition, in LAProof.C.build_csr]
___builtin_ctzll [definition, in LAProof.C.build_csr]
___builtin_ctzl [definition, in LAProof.C.build_csr]
___builtin_ctz [definition, in LAProof.C.build_csr]
___builtin_clzll [definition, in LAProof.C.build_csr]
___builtin_clzl [definition, in LAProof.C.build_csr]
___builtin_clz [definition, in LAProof.C.build_csr]
___builtin_clsll [definition, in LAProof.C.build_csr]
___builtin_clsl [definition, in LAProof.C.build_csr]
___builtin_cls [definition, in LAProof.C.build_csr]
___builtin_bswap64 [definition, in LAProof.C.build_csr]
___builtin_bswap32 [definition, in LAProof.C.build_csr]
___builtin_bswap16 [definition, in LAProof.C.build_csr]
___builtin_bswap [definition, in LAProof.C.build_csr]
___builtin_annot_intval [definition, in LAProof.C.build_csr]
___builtin_annot [definition, in LAProof.C.build_csr]
_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]
_scratch [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]
_frexp [definition, in LAProof.C.densemat]
_free [definition, in LAProof.C.densemat]
_fma [definition, in LAProof.C.densemat]
_fabs [definition, in LAProof.C.densemat]
_exit [definition, in LAProof.C.densemat]
_err [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_and_solve [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'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]
Module Index
A
AlternatePresentations [in LAProof.C.matrix_model]B
BPO [in LAProof.C.distinct]F
F [in LAProof.accuracy_proofs.mv_mathcomp]F [in LAProof.C.spec_densemat]
I
Info [in LAProof.C.sparse]Info [in LAProof.C.cholesky]
Info [in LAProof.C.alloc]
Info [in LAProof.C.build_csr]
Info [in LAProof.C.densemat]
Info [in LAProof.C.bandmat]
Variable Index
A
AlternatePresentations.WithNaN.NAN [in LAProof.C.matrix_model]AlternatePresentations.WithNaN.t [in LAProof.C.matrix_model]
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.fma_dot_acc]
ForwardError.Hfin [in LAProof.accuracy_proofs.dot_acc]
ForwardError.Hlen [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.Hlen [in LAProof.accuracy_proofs.dot_acc]
ForwardError.NAN [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.NAN [in LAProof.accuracy_proofs.dot_acc]
ForwardError.t [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.t [in LAProof.accuracy_proofs.dot_acc]
ForwardError.v1 [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.v1 [in LAProof.accuracy_proofs.dot_acc]
ForwardError.v2 [in LAProof.accuracy_proofs.fma_dot_acc]
ForwardError.v2 [in LAProof.accuracy_proofs.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.fma_dot_acc]
MixedError.Hfin [in LAProof.accuracy_proofs.dot_acc]
MixedError.Hlen [in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.Hlen [in LAProof.accuracy_proofs.dot_acc]
MixedError.NAN [in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.NAN [in LAProof.accuracy_proofs.dot_acc]
MixedError.t [in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.t [in LAProof.accuracy_proofs.dot_acc]
MixedError.v1 [in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.v1 [in LAProof.accuracy_proofs.dot_acc]
MixedError.v2 [in LAProof.accuracy_proofs.fma_dot_acc]
MixedError.v2 [in LAProof.accuracy_proofs.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
SBO.A [in LAProof.C.distinct]SBO.InhA [in LAProof.C.distinct]
SBO.le [in LAProof.C.distinct]
SBO.SBO [in LAProof.C.distinct]
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.libvalidsdp]
WithNan.NAN [in LAProof.accuracy_proofs.sum_acc]
WithNaN.NAN [in LAProof.accuracy_proofs.solve_model]
WithNAN.NAN [in LAProof.accuracy_proofs.gemv_acc]
WithNaN.t [in LAProof.accuracy_proofs.libvalidsdp]
WithNan.t [in LAProof.accuracy_proofs.sum_acc]
WithNaN.t [in LAProof.accuracy_proofs.solve_model]
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
bandmatbuild_csr
C
choleskycommon
D
densematdensemat_lemmas
distinct
dotprod_model
dot_acc
dot_acc_lemmas
E
exportF
floatlibfloat_acc_lems
fma_dot_acc
fma_is_finite
G
gemm_accgemv_acc
L
libvalidsdpM
matrix_modelmv_mathcomp
P
partial_csrpreamble
S
solve_modelsparse
sparse_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
verif_build_csr
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]
AlternatePresentations.subtract_loop_alt_original [in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_jik_original [in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_ffuns_ffuns' [in LAProof.C.matrix_model]
B
backward_subst_UT [in LAProof.accuracy_proofs.solve_model]BDIV_finite_e [in LAProof.accuracy_proofs.libvalidsdp]
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]
BFREXP_finite_strict_e [in LAProof.accuracy_proofs.solve_model]
BFREXP_finite_e [in LAProof.accuracy_proofs.solve_model]
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.common]
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]
BMULT_finite_strict_e [in LAProof.accuracy_proofs.solve_model]
Bmult_R0 [in LAProof.accuracy_proofs.solve_model]
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_coo_to_csr_matrix [in LAProof.C.verif_build_csr]
body_coo_count [in LAProof.C.verif_build_csr]
body_densematn_cfactor_and_solve [in LAProof.C.verif_densemat_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_csr_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_cholesky [in LAProof.C.verif_cholesky]
body_csr_matrix_vector_multiply_byrows [in LAProof.C.verif_sparse_byrows]
body_csr_row_vector_multiply [in LAProof.C.verif_sparse_byrows]
body_csr_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.common]
BPLUS_neg_zero [in LAProof.accuracy_proofs.common]
BPLUS_B2R_zero [in LAProof.accuracy_proofs.libvalidsdp]
bpow_fprec_lb [in LAProof.accuracy_proofs.fma_is_finite]
bpow_femax_lb [in LAProof.accuracy_proofs.fma_is_finite]
BPO_eqv_iff [in LAProof.C.partial_csr]
BPO.mkEqv [in LAProof.C.distinct]
BPO.mktesteqvspec [in LAProof.C.distinct]
BPO.mkteststrictspec [in LAProof.C.distinct]
BPO.StrictOrderstrict [in LAProof.C.distinct]
BSQRT_nonneg [in LAProof.accuracy_proofs.libvalidsdp]
BSQRT_finite_e [in LAProof.accuracy_proofs.libvalidsdp]
BSQRT_finite_e [in LAProof.accuracy_proofs.solve_model]
bSUM [in LAProof.accuracy_proofs.sum_acc]
build_csr_matrix_correct [in LAProof.C.sparse_model]
build_csr_row_correct [in LAProof.C.sparse_model]
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]
cholesky_return'_e [in LAProof.C.verif_densemat_cholesky]
cholesky_jik_spec_backwards_finite [in LAProof.accuracy_proofs.libvalidsdp]
cholesky_return_success [in LAProof.accuracy_proofs.solve_model]
cholesky_success_R_finite [in LAProof.accuracy_proofs.solve_model]
column_major_const [in LAProof.C.densemat_lemmas]
combine_split [in LAProof.accuracy_proofs.fma_is_finite]
coord_sorted_e [in LAProof.C.partial_csr]
coo_to_matrix_build_csr_matrix [in LAProof.C.partial_csr]
coo_upto_wellformed [in LAProof.C.partial_csr]
coo_entry_bounds [in LAProof.C.partial_csr]
coo_matrix_equiv_trans [in LAProof.C.sparse_model]
coo_matrix_equiv_symm [in LAProof.C.sparse_model]
coo_matrix_equiv_refl [in LAProof.C.sparse_model]
coo_to_matrix_equiv [in LAProof.C.sparse_model]
coo_matrix_wellformed_equiv [in LAProof.C.sparse_model]
count_distinct_range_same [in LAProof.C.distinct]
count_distinct_1 [in LAProof.C.distinct]
count_distinct_aux_lemma [in LAProof.C.distinct]
count_distinct_aux_mono [in LAProof.C.distinct]
count_distinct_noincr [in LAProof.C.distinct]
count_distinct_incr' [in LAProof.C.distinct]
count_distinct_incr [in LAProof.C.distinct]
count_distinct_mono [in LAProof.C.distinct]
count_distinct_bound' [in LAProof.C.distinct]
count_distinct_bound [in LAProof.C.distinct]
csr_row_rep_colsnonneg [in LAProof.C.partial_csr]
csr_multiply_loop_body [in LAProof.C.verif_sparse]
csr_row_rep_property [in LAProof.C.sparse_model]
csr_row_rep_col_range [in LAProof.C.sparse_model]
csr_row_rep_cols_nonneg [in LAProof.C.sparse_model]
csr_to_matrix_cols [in LAProof.C.sparse_model]
csr_to_matrix_rows [in LAProof.C.sparse_model]
ctype_of_the_type [in LAProof.C.spec_densemat]
cV_of_list_of_cV [in LAProof.accuracy_proofs.mv_mathcomp]
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_eq [in LAProof.accuracy_proofs.libvalidsdp]
default_abs_eq [in LAProof.accuracy_proofs.libvalidsdp]
default_abs_nonzero [in LAProof.accuracy_proofs.libvalidsdp]
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]
diag_finite_R_finite [in LAProof.accuracy_proofs.solve_model]
digits_max_mantissa [in LAProof.accuracy_proofs.libvalidsdp]
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_mixed_error_rel [in LAProof.accuracy_proofs.dot_acc_lemmas]
dotprod_forward_error_rel [in LAProof.accuracy_proofs.dot_acc_lemmas]
dotprod_congr [in LAProof.C.floatlib]
dotprod_forward_error [in LAProof.accuracy_proofs.dot_acc]
dotprod_mixed_error [in LAProof.accuracy_proofs.dot_acc]
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]
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
enum_mem_ordinal [in LAProof.C.matrix_model]eqv_cda [in LAProof.C.distinct]
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]
Fmulmx_matrix_vector_mult [in LAProof.accuracy_proofs.mv_mathcomp]
foldl_congr [in LAProof.accuracy_proofs.common]
fold_csr_rep' [in LAProof.C.verif_build_csr]
fold_coo_rep [in LAProof.C.verif_build_csr]
fold_left_preserves [in LAProof.C.densemat_lemmas]
Forall_take_ord_enum [in LAProof.accuracy_proofs.libvalidsdp]
format_FT2R [in LAProof.accuracy_proofs.libvalidsdp]
forward_subst_LT [in LAProof.accuracy_proofs.solve_model]
Fscalemx_mixed_error [in LAProof.accuracy_proofs.vec_op_acc]
fspec_eta_nonzero [in LAProof.accuracy_proofs.libvalidsdp]
fSUM [in LAProof.accuracy_proofs.sum_acc]
fsum_l2r_rec_finite_e1 [in LAProof.accuracy_proofs.libvalidsdp]
fsum_l2r_rec_finite_e [in LAProof.accuracy_proofs.libvalidsdp]
Fsum_forward_error [in LAProof.accuracy_proofs.sum_acc]
Fsum_backward_error [in LAProof.accuracy_proofs.sum_acc]
FS_val_ext [in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fsqrt' [in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fdiv' [in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fdiv [in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fopp' [in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fopp [in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fmult' [in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fmult [in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fplus' [in LAProof.accuracy_proofs.libvalidsdp]
FS_val_fplus [in LAProof.accuracy_proofs.libvalidsdp]
FS_val_mkFS [in LAProof.accuracy_proofs.libvalidsdp]
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_BDIV_congr [in LAProof.accuracy_proofs.libvalidsdp]
FT2R_feq [in LAProof.accuracy_proofs.libvalidsdp]
FT2R_congr [in LAProof.accuracy_proofs.libvalidsdp]
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.FMA_mulmx_fma_dotprod [in LAProof.accuracy_proofs.mv_mathcomp]
F.FMA_mulmx_col [in LAProof.accuracy_proofs.mv_mathcomp]
F.FMA_mulmx_row [in LAProof.accuracy_proofs.mv_mathcomp]
F.mulmx_dotprodF [in LAProof.accuracy_proofs.mv_mathcomp]
F.mulmx_col [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
last_R_finite [in LAProof.accuracy_proofs.solve_model]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]
le1_sorted [in LAProof.C.distinct]
listlist_of_mx_inj [in LAProof.accuracy_proofs.mv_mathcomp]
listlist_of_mx_col_mx [in LAProof.accuracy_proofs.mv_mathcomp]
listlist_of_mx_of_listlist [in LAProof.accuracy_proofs.mv_mathcomp]
list_of_cV_col_mx [in LAProof.accuracy_proofs.mv_mathcomp]
list_of_cV_of_list [in LAProof.accuracy_proofs.mv_mathcomp]
LVDSP_cholesky_success [in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_cholesky_spec [in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_lemma_2_1 [in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_ytildes_eq [in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_ytilded_eq [in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_stilde_eq [in LAProof.accuracy_proofs.libvalidsdp]
LVSDP_fcmsum_eq [in LAProof.accuracy_proofs.libvalidsdp]
M
map_inj [in LAProof.C.matrix_model]map_const_len [in LAProof.accuracy_proofs.mv_mathcomp]
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_cols_listlist_of_mx [in LAProof.accuracy_proofs.mv_mathcomp]
matrix_rows_listlist_of_mx [in LAProof.accuracy_proofs.mv_mathcomp]
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]
matrix_index_Z [in LAProof.C.partial_csr]
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]
max_mantissa_bounded [in LAProof.accuracy_proofs.libvalidsdp]
MINUS_PLUS_BOPP [in LAProof.accuracy_proofs.common]
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]
mx_of_listlist_of_mx [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_list_of_cV [in LAProof.accuracy_proofs.mv_mathcomp]
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]
ord_enum_S [in LAProof.accuracy_proofs.libvalidsdp]
P
partial_CSR_VAL_defined [in LAProof.C.partial_csr]partial_CSR_properties [in LAProof.C.partial_csr]
partial_CSR_lastrows [in LAProof.C.partial_csr]
partial_CSR_newrow [in LAProof.C.partial_csr]
partial_CSR_skiprow [in LAProof.C.partial_csr]
partial_CSR_0 [in LAProof.C.partial_csr]
partial_CSR_newcol [in LAProof.C.partial_csr]
partial_CSR_duplicate [in LAProof.C.partial_csr]
partial_CSR_rowptr' [in LAProof.C.partial_csr]
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]
prec_lt_emax [in LAProof.accuracy_proofs.libvalidsdp]
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]
reflect_coord_le [in LAProof.C.sparse_model]
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]
rev_List_rev [in LAProof.accuracy_proofs.solve_model]
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]
rowptr_sorted_e1 [in LAProof.C.sparse_model]
rowptr_sorted_e [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_list_of_cV [in LAProof.accuracy_proofs.mv_mathcomp]
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_sublist [in LAProof.C.distinct]
sorted_e1 [in LAProof.C.distinct]
sorted_app_e3 [in LAProof.C.distinct]
sorted_app [in LAProof.C.distinct]
sorted_i [in LAProof.C.distinct]
sorted_e [in LAProof.C.distinct]
sorted_cons_e2 [in LAProof.C.partial_csr]
sorted_app_e1 [in LAProof.C.sparse_model]
sparse_fma_dotprod_forward_error [in LAProof.accuracy_proofs.dot_acc_lemmas]
sparse_dotprod_forward_error_rel [in LAProof.accuracy_proofs.dot_acc_lemmas]
sparse_dotprod_forward_error [in LAProof.accuracy_proofs.dot_acc]
SQRT_nonneg [in LAProof.accuracy_proofs.solve_model]
stilde_subtract_loop [in LAProof.accuracy_proofs.libvalidsdp]
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_another [in LAProof.C.verif_cholesky]
subtract_loop_finite_e [in LAProof.accuracy_proofs.solve_model]
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]
sum_any_accuracy [in LAProof.C.sparse_model]
surely_malloc_spec_sub [in LAProof.C.spec_alloc]
T
take_snoc [in LAProof.C.matrix_model]take_ord_enum [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]
Y
ytilded_subtract_loop [in LAProof.accuracy_proofs.libvalidsdp]ytildes_subtract_loop [in LAProof.accuracy_proofs.libvalidsdp]
Z
Zlength_seq [in LAProof.C.floatlib]Zlength_iota [in LAProof.C.verif_cholesky]
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_vector_sub [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_column_major [in LAProof.C.densemat_lemmas]
Znth_ord_enum [in LAProof.C.densemat_lemmas]
Constructor Index
B
build_partial_CSR [in LAProof.C.partial_csr]build_coo_csr [in LAProof.C.partial_csr]
build_csr_matrix_wellformed [in LAProof.C.sparse_model]
C
csr_row_rep_val [in LAProof.C.sparse_model]csr_row_rep_zero [in LAProof.C.sparse_model]
csr_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
sorted_cons [in LAProof.C.distinct]sorted_1 [in LAProof.C.distinct]
sorted_nil [in LAProof.C.distinct]
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]
Sum_Any_perm [in LAProof.C.sparse_model]
Sum_Any_split [in LAProof.C.sparse_model]
Sum_Any_1 [in LAProof.C.sparse_model]
Sum_Any_0 [in LAProof.C.sparse_model]
Axiom Index
B
body_exit [in LAProof.C.verif_alloc]Inductive Index
C
coo_csr [in LAProof.C.partial_csr]csr_matrix_wellformed [in LAProof.C.sparse_model]
csr_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]P
partial_CSR [in LAProof.C.partial_csr]R
R_dot_prod_rel [in LAProof.accuracy_proofs.dotprod_model]S
sorted [in LAProof.C.distinct]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]
sum_any [in LAProof.C.sparse_model]
Projection Index
B
BPO.BO [in LAProof.C.distinct]BPO.Eqv [in LAProof.C.distinct]
BPO.eqv [in LAProof.C.distinct]
BPO.eqvb [in LAProof.C.distinct]
BPO.eqvbspec [in LAProof.C.distinct]
BPO.lt [in LAProof.C.distinct]
BPO.ltb [in LAProof.C.distinct]
BPO.ltb_spec [in LAProof.C.distinct]
BPO.PO [in LAProof.C.distinct]
BPO.Strict [in LAProof.C.distinct]
C
coo_entries [in LAProof.C.sparse_model]coo_cols [in LAProof.C.sparse_model]
coo_rows [in LAProof.C.sparse_model]
csr_rows [in LAProof.C.sparse_model]
csr_row_ptr [in LAProof.C.sparse_model]
csr_col_ind [in LAProof.C.sparse_model]
csr_vals [in LAProof.C.sparse_model]
csr_cols [in LAProof.C.sparse_model]
T
test [in LAProof.C.distinct]test_spec [in LAProof.C.distinct]
Section Index
A
AlternatePresentations.WithNaN [in LAProof.C.matrix_model]D
DotProdFloat [in LAProof.accuracy_proofs.dotprod_model]DotProdFMA [in LAProof.accuracy_proofs.dotprod_model]
F
ForwardError [in LAProof.accuracy_proofs.fma_dot_acc]ForwardError [in LAProof.accuracy_proofs.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.fma_dot_acc]MixedError [in LAProof.accuracy_proofs.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
SBO [in LAProof.C.distinct]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.libvalidsdp]WithNan [in LAProof.accuracy_proofs.sum_acc]
WithNaN [in LAProof.accuracy_proofs.solve_model]
WithNAN [in LAProof.accuracy_proofs.gemv_acc]
WithNans [in LAProof.accuracy_proofs.vec_op_acc]
WithNaN.A [in LAProof.accuracy_proofs.libvalidsdp]
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_empty' [in LAProof.C.densemat_lemmas]change_composite_env_empty [in LAProof.C.densemat_lemmas]
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.spec_sparse]
CompSpecs [in LAProof.C.verif_cholesky]
CoordBO [in LAProof.C.sparse_model]
CoordBPO [in LAProof.C.sparse_model]
CoordPO [in LAProof.C.sparse_model]
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.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.dot_acc]
D [in LAProof.accuracy_proofs.sum_acc]
E
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]
E [in LAProof.accuracy_proofs.dot_acc]
eps [in LAProof.accuracy_proofs.libvalidsdp]
eta [in LAProof.accuracy_proofs.libvalidsdp]
F
F [in LAProof.accuracy_proofs.libvalidsdp]G
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.vec_op_acc]
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.sum_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.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.gemm_acc]
g1 [in LAProof.accuracy_proofs.dot_acc]
g1 [in LAProof.accuracy_proofs.dot_acc]
g1 [in LAProof.accuracy_proofs.vecnorm_acc]
g1 [in LAProof.accuracy_proofs.gemv_acc]
N
n [in LAProof.accuracy_proofs.fma_dot_acc]n [in LAProof.accuracy_proofs.dot_acc]
n [in LAProof.accuracy_proofs.vecnorm_acc]
n [in LAProof.accuracy_proofs.vecnorm_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.dot_acc]
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.fma_dot_acc]
nnzR [in LAProof.accuracy_proofs.dot_acc_lemmas]
nnzR [in LAProof.accuracy_proofs.dot_acc_lemmas]
nnzR [in LAProof.accuracy_proofs.dot_acc]
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.fma_dot_acc]
v1R [in LAProof.accuracy_proofs.dot_acc_lemmas]
v1R [in LAProof.accuracy_proofs.dot_acc_lemmas]
v1R [in LAProof.accuracy_proofs.dot_acc]
v1R [in LAProof.accuracy_proofs.dotprod_model]
v1R' [in LAProof.accuracy_proofs.fma_dot_acc]
v1R' [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]
v2R' [in LAProof.accuracy_proofs.dot_acc]
X
xR [in LAProof.accuracy_proofs.vecnorm_acc]xR [in LAProof.accuracy_proofs.vecnorm_acc]
Definition Index
A
add_to_coo_matrix_spec [in LAProof.C.spec_sparse]add_to_coo [in LAProof.C.spec_sparse]
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]
AlternatePresentations.subtract_loop_original [in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_listpairs [in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_alt [in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_ffuns [in LAProof.C.matrix_model]
AlternatePresentations.subtract_loop_ffuns' [in LAProof.C.matrix_model]
B
backward_subst [in LAProof.accuracy_proofs.solve_model]backward_subst_step [in LAProof.accuracy_proofs.solve_model]
Beq_dec_t [in LAProof.accuracy_proofs.common]
BFREXP [in LAProof.accuracy_proofs.solve_model]
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]
build_csr_matrix [in LAProof.C.sparse_model]
build_csr_rows [in LAProof.C.sparse_model]
build_csr_row [in LAProof.C.sparse_model]
C
cd_upto [in LAProof.C.partial_csr]cholesky_jik_ij_any [in LAProof.C.matrix_model]
cholesky_jik_upto [in LAProof.C.matrix_model]
cholesky_return' [in LAProof.C.verif_densemat_cholesky]
cholesky_bound [in LAProof.accuracy_proofs.libvalidsdp]
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]
cholesky_return [in LAProof.accuracy_proofs.solve_model]
cholesky_success [in LAProof.accuracy_proofs.solve_model]
cholesky_jik_upto [in LAProof.accuracy_proofs.solve_model]
cholesky_jik_spec [in LAProof.accuracy_proofs.solve_model]
cholesky_jik_ij [in LAProof.accuracy_proofs.solve_model]
column_major [in LAProof.C.spec_densemat]
composites [in LAProof.C.sparse]
composites [in LAProof.C.cholesky]
composites [in LAProof.C.alloc]
composites [in LAProof.C.build_csr]
composites [in LAProof.C.densemat]
composites [in LAProof.C.bandmat]
coord_leb [in LAProof.C.sparse_model]
coord_le [in LAProof.C.sparse_model]
coord_eqb [in LAProof.C.sparse_model]
coo_less_spec [in LAProof.C.spec_sparse]
coo_count_spec [in LAProof.C.spec_sparse]
coo_quicksort_spec [in LAProof.C.spec_sparse]
coo_to_csr_matrix_spec [in LAProof.C.spec_sparse]
coo_rep [in LAProof.C.spec_sparse]
coo_csr_sind [in LAProof.C.partial_csr]
coo_csr_rec [in LAProof.C.partial_csr]
coo_csr_ind [in LAProof.C.partial_csr]
coo_csr_rect [in LAProof.C.partial_csr]
coo_upto [in LAProof.C.partial_csr]
coo_to_matrix [in LAProof.C.sparse_model]
coo_matrix_equiv [in LAProof.C.sparse_model]
coo_matrix_wellformed [in LAProof.C.sparse_model]
count_distinct [in LAProof.C.distinct]
count_distinct_aux [in LAProof.C.distinct]
crazy [in LAProof.accuracy_proofs.mv_mathcomp]
create_coo_matrix_spec [in LAProof.C.spec_sparse]
csr_matrix_vector_multiply_spec [in LAProof.C.spec_sparse]
csr_matrix_vector_multiply_byrows_spec [in LAProof.C.spec_sparse]
csr_row_vector_multiply_spec [in LAProof.C.spec_sparse]
csr_matrix_rows_spec [in LAProof.C.spec_sparse]
csr_token [in LAProof.C.spec_sparse]
csr_token' [in LAProof.C.spec_sparse]
csr_rep [in LAProof.C.spec_sparse]
csr_rep' [in LAProof.C.spec_sparse]
csr_matrix_wellformed_sind [in LAProof.C.sparse_model]
csr_matrix_wellformed_rec [in LAProof.C.sparse_model]
csr_matrix_wellformed_ind [in LAProof.C.sparse_model]
csr_matrix_wellformed_rect [in LAProof.C.sparse_model]
csr_to_matrix [in LAProof.C.sparse_model]
csr_row_rep_sind [in LAProof.C.sparse_model]
csr_row_rep_ind [in LAProof.C.sparse_model]
ctype_of_type [in LAProof.C.spec_densemat]
cV_of_list [in LAProof.accuracy_proofs.mv_mathcomp]
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]
default_abs [in LAProof.accuracy_proofs.libvalidsdp]
default_rel [in LAProof.accuracy_proofs.libvalidsdp]
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_cfactor_and_solve_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.C.floatlib]
dotprod [in LAProof.accuracy_proofs.dotprod_model]
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
entries_correspond [in LAProof.C.partial_csr]exit_spec [in LAProof.C.spec_alloc]
F
fcmsum_l2r [in LAProof.accuracy_proofs.libvalidsdp]Float_max [in LAProof.accuracy_proofs.libvalidsdp]
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.accuracy_proofs.solve_model]
forward_subst_step [in LAProof.accuracy_proofs.solve_model]
frobenius_norm [in LAProof.C.spec_densemat]
frobenius_norm2 [in LAProof.C.spec_densemat]
FR2 [in LAProof.accuracy_proofs.dotprod_model]
fspec [in LAProof.accuracy_proofs.libvalidsdp]
fsum_l2r_rec [in LAProof.accuracy_proofs.libvalidsdp]
fun_bnd [in LAProof.accuracy_proofs.fma_is_finite]
f_coo_to_csr_matrix [in LAProof.C.sparse]
f_coo_count [in LAProof.C.sparse]
f_coo_quicksort [in LAProof.C.sparse]
f_coo_less [in LAProof.C.sparse]
f_swap [in LAProof.C.sparse]
f_add_to_coo_matrix [in LAProof.C.sparse]
f_create_coo_matrix [in LAProof.C.sparse]
f_csr_matrix_vector_multiply_byrows [in LAProof.C.sparse]
f_csr_row_vector_multiply [in LAProof.C.sparse]
f_csr_matrix_rows [in LAProof.C.sparse]
f_csr_matrix_vector_multiply [in LAProof.C.sparse]
f_cholesky [in LAProof.C.cholesky]
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_coo_to_csr_matrix [in LAProof.C.build_csr]
f_coo_count [in LAProof.C.build_csr]
f_coo_quicksort [in LAProof.C.build_csr]
f_coo_less [in LAProof.C.build_csr]
f_swap [in LAProof.C.build_csr]
f_add_to_coo_matrix [in LAProof.C.build_csr]
f_create_coo_matrix [in LAProof.C.build_csr]
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_densematn_cfactor_and_solve [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_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' [in LAProof.accuracy_proofs.libvalidsdp]
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.FMA_mulmx [in LAProof.accuracy_proofs.mv_mathcomp]
F.FMA_dotprod [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.cholesky]
global_definitions [in LAProof.C.alloc]
global_definitions [in LAProof.C.build_csr]
global_definitions [in LAProof.C.densemat]
global_definitions [in LAProof.C.bandmat]
Gprog [in LAProof.C.spec_sparse]
Gprog [in LAProof.C.verif_alloc]
Gprog [in LAProof.C.verif_cholesky]
Gprog [in LAProof.C.densemat_lemmas]
g1 [in LAProof.accuracy_proofs.common]
I
Info.abi [in LAProof.C.sparse]Info.abi [in LAProof.C.cholesky]
Info.abi [in LAProof.C.alloc]
Info.abi [in LAProof.C.build_csr]
Info.abi [in LAProof.C.densemat]
Info.abi [in LAProof.C.bandmat]
Info.arch [in LAProof.C.sparse]
Info.arch [in LAProof.C.cholesky]
Info.arch [in LAProof.C.alloc]
Info.arch [in LAProof.C.build_csr]
Info.arch [in LAProof.C.densemat]
Info.arch [in LAProof.C.bandmat]
Info.big_endian [in LAProof.C.sparse]
Info.big_endian [in LAProof.C.cholesky]
Info.big_endian [in LAProof.C.alloc]
Info.big_endian [in LAProof.C.build_csr]
Info.big_endian [in LAProof.C.densemat]
Info.big_endian [in LAProof.C.bandmat]
Info.bitsize [in LAProof.C.sparse]
Info.bitsize [in LAProof.C.cholesky]
Info.bitsize [in LAProof.C.alloc]
Info.bitsize [in LAProof.C.build_csr]
Info.bitsize [in LAProof.C.densemat]
Info.bitsize [in LAProof.C.bandmat]
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.cholesky]
Info.build_tag [in LAProof.C.cholesky]
Info.build_number [in LAProof.C.cholesky]
Info.build_branch [in LAProof.C.alloc]
Info.build_tag [in LAProof.C.alloc]
Info.build_number [in LAProof.C.alloc]
Info.build_branch [in LAProof.C.build_csr]
Info.build_tag [in LAProof.C.build_csr]
Info.build_number [in LAProof.C.build_csr]
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.bandmat]
Info.build_tag [in LAProof.C.bandmat]
Info.build_number [in LAProof.C.bandmat]
Info.model [in LAProof.C.sparse]
Info.model [in LAProof.C.cholesky]
Info.model [in LAProof.C.alloc]
Info.model [in LAProof.C.build_csr]
Info.model [in LAProof.C.densemat]
Info.model [in LAProof.C.bandmat]
Info.normalized [in LAProof.C.sparse]
Info.normalized [in LAProof.C.cholesky]
Info.normalized [in LAProof.C.alloc]
Info.normalized [in LAProof.C.build_csr]
Info.normalized [in LAProof.C.densemat]
Info.normalized [in LAProof.C.bandmat]
Info.source_file [in LAProof.C.sparse]
Info.source_file [in LAProof.C.cholesky]
Info.source_file [in LAProof.C.alloc]
Info.source_file [in LAProof.C.build_csr]
Info.source_file [in LAProof.C.densemat]
Info.source_file [in LAProof.C.bandmat]
Info.version [in LAProof.C.sparse]
Info.version [in LAProof.C.cholesky]
Info.version [in LAProof.C.alloc]
Info.version [in LAProof.C.build_csr]
Info.version [in LAProof.C.densemat]
Info.version [in LAProof.C.bandmat]
int_calloc_spec [in LAProof.C.spec_alloc]
iota [in LAProof.C.verif_cholesky]
iszero [in LAProof.accuracy_proofs.common]
iszero [in LAProof.accuracy_proofs.libvalidsdp]
J
joinLU [in LAProof.C.matrix_model]L
listlist_of_mx [in LAProof.accuracy_proofs.mv_mathcomp]lists_of_fun [in LAProof.C.verif_cholesky]
list_dotprod [in LAProof.accuracy_proofs.mv_mathcomp]
list_of_cV [in LAProof.accuracy_proofs.mv_mathcomp]
list_of_fun [in LAProof.C.verif_cholesky]
lshift1 [in LAProof.C.matrix_model]
LVSDP_NAN [in LAProof.accuracy_proofs.libvalidsdp]
M
map2 [in LAProof.C.floatlib]matrix [in LAProof.C.floatlib]
matrix [in LAProof.C.verif_cholesky]
matrix_vector_mult [in LAProof.accuracy_proofs.mv_mathcomp]
matrix_cols_nat [in LAProof.accuracy_proofs.mv_mathcomp]
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]
matrix_upd [in LAProof.C.partial_csr]
max_mantissa [in LAProof.accuracy_proofs.libvalidsdp]
mirror_UT [in LAProof.C.matrix_model]
mkFS [in LAProof.accuracy_proofs.libvalidsdp]
mx_of_listlist [in LAProof.accuracy_proofs.mv_mathcomp]
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]
no_extra_zeros [in LAProof.C.partial_csr]
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]
origFIS [in LAProof.accuracy_proofs.libvalidsdp]
P
partial_CSR_sind [in LAProof.C.partial_csr]partial_CSR_ind [in LAProof.C.partial_csr]
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.cholesky]
prog [in LAProof.C.alloc]
prog [in LAProof.C.build_csr]
prog [in LAProof.C.densemat]
prog [in LAProof.C.bandmat]
public_idents [in LAProof.C.sparse]
public_idents [in LAProof.C.cholesky]
public_idents [in LAProof.C.alloc]
public_idents [in LAProof.C.build_csr]
public_idents [in LAProof.C.densemat]
public_idents [in LAProof.C.bandmat]
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]sorted_sind [in LAProof.C.distinct]
sorted_ind [in LAProof.C.distinct]
SparseASI [in LAProof.C.spec_sparse]
SparseVSU [in LAProof.C.VSU_sparse]
sparse_imports [in LAProof.C.spec_sparse]
stilde [in LAProof.accuracy_proofs.libvalidsdp]
subtractoff_spec [in LAProof.C.spec_densemat]
subtract_loop_any [in LAProof.C.matrix_model]
subtract_loop [in LAProof.C.verif_cholesky]
subtract_loop_jik [in LAProof.accuracy_proofs.solve_model]
subtract_loop [in LAProof.accuracy_proofs.solve_model]
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]
sum_any_sind [in LAProof.C.sparse_model]
sum_any_ind [in LAProof.C.sparse_model]
surely_malloc_spec [in LAProof.C.spec_alloc]
surely_malloc_spec' [in LAProof.C.spec_alloc]
swap_spec [in LAProof.C.spec_sparse]
T
the_type [in LAProof.C.spec_densemat]the_ctype [in LAProof.C.spec_densemat]
the_loop_body [in LAProof.C.verif_sparse]
the_FIS [in LAProof.accuracy_proofs.libvalidsdp]
two_normR [in LAProof.accuracy_proofs.vecnorm_acc]
two_normF [in LAProof.accuracy_proofs.vecnorm_acc]
t_coo [in LAProof.C.spec_sparse]
t_csr [in LAProof.C.spec_sparse]
U
update_mx [in LAProof.accuracy_proofs.solve_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.spec_sparse]
Vprog [in LAProof.C.verif_cholesky]
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]
W
widen_ik [in LAProof.C.matrix_model]Y
ytilded [in LAProof.accuracy_proofs.libvalidsdp]ytildes [in LAProof.accuracy_proofs.libvalidsdp]
Z
Zcholesky_return [in LAProof.accuracy_proofs.solve_model]_
_t'9 [in LAProof.C.sparse]_t'8 [in LAProof.C.sparse]
_t'7 [in LAProof.C.sparse]
_t'6 [in LAProof.C.sparse]
_t'5 [in LAProof.C.sparse]
_t'4 [in LAProof.C.sparse]
_t'3 [in LAProof.C.sparse]
_t'2 [in LAProof.C.sparse]
_t'15 [in LAProof.C.sparse]
_t'14 [in LAProof.C.sparse]
_t'13 [in LAProof.C.sparse]
_t'12 [in LAProof.C.sparse]
_t'11 [in LAProof.C.sparse]
_t'10 [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]
_swap [in LAProof.C.sparse]
_surely_malloc [in LAProof.C.sparse]
_s [in LAProof.C.sparse]
_rows [in LAProof.C.sparse]
_row_ptr [in LAProof.C.sparse]
_row_ind [in LAProof.C.sparse]
_right [in LAProof.C.sparse]
_ri [in LAProof.C.sparse]
_rb [in LAProof.C.sparse]
_ra [in LAProof.C.sparse]
_r [in LAProof.C.sparse]
_q [in LAProof.C.sparse]
_pval [in LAProof.C.sparse]
_prow_ind [in LAProof.C.sparse]
_pcol_ind [in LAProof.C.sparse]
_p [in LAProof.C.sparse]
_next [in LAProof.C.sparse]
_n [in LAProof.C.sparse]
_mid [in LAProof.C.sparse]
_maxn [in LAProof.C.sparse]
_main [in LAProof.C.sparse]
_m [in LAProof.C.sparse]
_lo [in LAProof.C.sparse]
_left [in LAProof.C.sparse]
_l [in LAProof.C.sparse]
_k [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]
_exit [in LAProof.C.sparse]
_csr_row_vector_multiply [in LAProof.C.sparse]
_csr_matrix_vector_multiply_byrows [in LAProof.C.sparse]
_csr_matrix_vector_multiply [in LAProof.C.sparse]
_csr_matrix_rows [in LAProof.C.sparse]
_csr_matrix [in LAProof.C.sparse]
_create_coo_matrix [in LAProof.C.sparse]
_count [in LAProof.C.sparse]
_coo_to_csr_matrix [in LAProof.C.sparse]
_coo_quicksort [in LAProof.C.sparse]
_coo_matrix [in LAProof.C.sparse]
_coo_less [in LAProof.C.sparse]
_coo_count [in LAProof.C.sparse]
_cols [in LAProof.C.sparse]
_col_ind [in LAProof.C.sparse]
_ci [in LAProof.C.sparse]
_c [in LAProof.C.sparse]
_base [in LAProof.C.sparse]
_b [in LAProof.C.sparse]
_add_to_coo_matrix [in LAProof.C.sparse]
_a [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'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'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]
_t'9 [in LAProof.C.build_csr]
_t'8 [in LAProof.C.build_csr]
_t'7 [in LAProof.C.build_csr]
_t'6 [in LAProof.C.build_csr]
_t'5 [in LAProof.C.build_csr]
_t'4 [in LAProof.C.build_csr]
_t'3 [in LAProof.C.build_csr]
_t'2 [in LAProof.C.build_csr]
_t'15 [in LAProof.C.build_csr]
_t'14 [in LAProof.C.build_csr]
_t'13 [in LAProof.C.build_csr]
_t'12 [in LAProof.C.build_csr]
_t'11 [in LAProof.C.build_csr]
_t'10 [in LAProof.C.build_csr]
_t'1 [in LAProof.C.build_csr]
_x [in LAProof.C.build_csr]
_val [in LAProof.C.build_csr]
_swap [in LAProof.C.build_csr]
_surely_malloc [in LAProof.C.build_csr]
_rows [in LAProof.C.build_csr]
_row_ptr [in LAProof.C.build_csr]
_row_ind [in LAProof.C.build_csr]
_right [in LAProof.C.build_csr]
_ri [in LAProof.C.build_csr]
_rb [in LAProof.C.build_csr]
_ra [in LAProof.C.build_csr]
_r [in LAProof.C.build_csr]
_q [in LAProof.C.build_csr]
_pval [in LAProof.C.build_csr]
_prow_ind [in LAProof.C.build_csr]
_pcol_ind [in LAProof.C.build_csr]
_p [in LAProof.C.build_csr]
_n [in LAProof.C.build_csr]
_mid [in LAProof.C.build_csr]
_maxn [in LAProof.C.build_csr]
_main [in LAProof.C.build_csr]
_lo [in LAProof.C.build_csr]
_left [in LAProof.C.build_csr]
_l [in LAProof.C.build_csr]
_k [in LAProof.C.build_csr]
_j [in LAProof.C.build_csr]
_i [in LAProof.C.build_csr]
_hi [in LAProof.C.build_csr]
_exit [in LAProof.C.build_csr]
_csr_matrix [in LAProof.C.build_csr]
_create_coo_matrix [in LAProof.C.build_csr]
_count [in LAProof.C.build_csr]
_coo_to_csr_matrix [in LAProof.C.build_csr]
_coo_quicksort [in LAProof.C.build_csr]
_coo_matrix [in LAProof.C.build_csr]
_coo_less [in LAProof.C.build_csr]
_coo_count [in LAProof.C.build_csr]
_cols [in LAProof.C.build_csr]
_col_ind [in LAProof.C.build_csr]
_ci [in LAProof.C.build_csr]
_c [in LAProof.C.build_csr]
_base [in LAProof.C.build_csr]
_b [in LAProof.C.build_csr]
_add_to_coo_matrix [in LAProof.C.build_csr]
_a [in LAProof.C.build_csr]
___compcert_va_int64 [in LAProof.C.build_csr]
___compcert_va_int32 [in LAProof.C.build_csr]
___compcert_va_float64 [in LAProof.C.build_csr]
___compcert_va_composite [in LAProof.C.build_csr]
___compcert_i64_utof [in LAProof.C.build_csr]
___compcert_i64_utod [in LAProof.C.build_csr]
___compcert_i64_umulh [in LAProof.C.build_csr]
___compcert_i64_umod [in LAProof.C.build_csr]
___compcert_i64_udiv [in LAProof.C.build_csr]
___compcert_i64_stof [in LAProof.C.build_csr]
___compcert_i64_stod [in LAProof.C.build_csr]
___compcert_i64_smulh [in LAProof.C.build_csr]
___compcert_i64_smod [in LAProof.C.build_csr]
___compcert_i64_shr [in LAProof.C.build_csr]
___compcert_i64_shl [in LAProof.C.build_csr]
___compcert_i64_sdiv [in LAProof.C.build_csr]
___compcert_i64_sar [in LAProof.C.build_csr]
___compcert_i64_dtou [in LAProof.C.build_csr]
___compcert_i64_dtos [in LAProof.C.build_csr]
___builtin_va_start [in LAProof.C.build_csr]
___builtin_va_end [in LAProof.C.build_csr]
___builtin_va_copy [in LAProof.C.build_csr]
___builtin_va_arg [in LAProof.C.build_csr]
___builtin_unreachable [in LAProof.C.build_csr]
___builtin_sqrt [in LAProof.C.build_csr]
___builtin_sel [in LAProof.C.build_csr]
___builtin_memcpy_aligned [in LAProof.C.build_csr]
___builtin_membar [in LAProof.C.build_csr]
___builtin_fsqrt [in LAProof.C.build_csr]
___builtin_fnmsub [in LAProof.C.build_csr]
___builtin_fnmadd [in LAProof.C.build_csr]
___builtin_fmsub [in LAProof.C.build_csr]
___builtin_fmin [in LAProof.C.build_csr]
___builtin_fmax [in LAProof.C.build_csr]
___builtin_fmadd [in LAProof.C.build_csr]
___builtin_fabsf [in LAProof.C.build_csr]
___builtin_fabs [in LAProof.C.build_csr]
___builtin_expect [in LAProof.C.build_csr]
___builtin_debug [in LAProof.C.build_csr]
___builtin_ctzll [in LAProof.C.build_csr]
___builtin_ctzl [in LAProof.C.build_csr]
___builtin_ctz [in LAProof.C.build_csr]
___builtin_clzll [in LAProof.C.build_csr]
___builtin_clzl [in LAProof.C.build_csr]
___builtin_clz [in LAProof.C.build_csr]
___builtin_clsll [in LAProof.C.build_csr]
___builtin_clsl [in LAProof.C.build_csr]
___builtin_cls [in LAProof.C.build_csr]
___builtin_bswap64 [in LAProof.C.build_csr]
___builtin_bswap32 [in LAProof.C.build_csr]
___builtin_bswap16 [in LAProof.C.build_csr]
___builtin_bswap [in LAProof.C.build_csr]
___builtin_annot_intval [in LAProof.C.build_csr]
___builtin_annot [in LAProof.C.build_csr]
_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]
_scratch [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]
_frexp [in LAProof.C.densemat]
_free [in LAProof.C.densemat]
_fma [in LAProof.C.densemat]
_fabs [in LAProof.C.densemat]
_exit [in LAProof.C.densemat]
_err [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_and_solve [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'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]
Record Index
B
BoolOrder [in LAProof.C.distinct]BPO.BoolPreOrder [in LAProof.C.distinct]
C
coo_matrix [in LAProof.C.sparse_model]csr_matrix [in LAProof.C.sparse_model]
| 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 | (1974 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 | (10 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 | (126 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 | (43 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 | (469 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 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) |
| 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 | (15 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 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 | (32 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 | (14 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 | (87 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 | (1118 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
This page has been generated by coqdoc