-
Notifications
You must be signed in to change notification settings - Fork 15
/
_CoqProject
98 lines (96 loc) · 2.53 KB
/
_CoqProject
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
-arg -w -arg -projection-no-head-constant
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -notation-overridden
-arg -w -arg -ambiguous-paths
-arg -w -arg -notation-incompatible-format
lib/ssrZ.v
lib/ssrR.v
lib/realType_ext.v
lib/Reals_ext.v
lib/logb.v
lib/Ranalysis_ext.v
lib/ssr_ext.v
lib/f2.v
lib/ssralg_ext.v
lib/bigop_ext.v
lib/natbin.v
lib/binary_entropy_function.v
lib/num_occ.v
lib/hamming.v
lib/poly_ext.v
lib/euclid.v
lib/dft.v
lib/classical_sets_ext.v
probability/fdist.v
probability/proba.v
probability/fsdist.v
probability/convex.v
probability/convex_equiv.v
probability/convex_stone.v
probability/jfdist_cond.v
probability/graphoid.v
probability/jensen.v
probability/ln_facts.v
probability/divergence.v
probability/variation_dist.v
probability/log_sum.v
probability/partition_inequality.v
probability/pinsker.v
probability/necset.v
probability/bayes.v
information_theory/source_code.v
information_theory/entropy.v
information_theory/channel.v
information_theory/pproba.v
information_theory/channel_code.v
information_theory/erasure_channel.v
information_theory/binary_symmetric_channel.v
information_theory/aep.v
information_theory/typ_seq.v
information_theory/types.v
information_theory/jtypes.v
information_theory/conditional_divergence.v
information_theory/source_coding_fl_direct.v
information_theory/source_coding_fl_converse.v
information_theory/channel_coding_direct.v
information_theory/joint_typ_seq.v
information_theory/error_exponent.v
information_theory/success_decode_bound.v
information_theory/channel_coding_converse.v
information_theory/kraft.v
information_theory/shannon_fano.v
information_theory/string_entropy.v
information_theory/entropy_convex.v
information_theory/source_coding_vl_direct.v
information_theory/source_coding_vl_converse.v
ecc_classic/linearcode.v
ecc_classic/decoding.v
ecc_classic/mceliece.v
ecc_classic/cyclic_code.v
ecc_classic/poly_decoding.v
ecc_classic/hamming_code.v
ecc_classic/repcode.v
ecc_classic/grs.v
ecc_classic/reed_solomon.v
ecc_classic/bch.v
ecc_classic/alternant.v
ecc_modern/subgraph_partition.v
ecc_modern/tanner.v
ecc_modern/tanner_partition.v
ecc_modern/summary.v
ecc_modern/checksum.v
ecc_modern/summary_tanner.v
ecc_modern/ldpc.v
ecc_modern/ldpc_algo.v
ecc_modern/ldpc_algo_proof.v
ecc_modern/ldpc_erasure.v
ecc_modern/max_subset.v
ecc_modern/stopping_set.v
ecc_modern/degree_profile.v
robust/robustmean.v
robust/weightedmean.v
toy_examples/expected_value_variance.v
toy_examples/expected_value_variance_ordn.v
toy_examples/expected_value_variance_tuple.v
toy_examples/conditional_entropy.v
-R . infotheo