A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64
stars
15
forks
source link
Reserved Notation ``_ `^ _`` has incompatible levels between fdist (infotheo) and sequences (mathcomp-analysis) #115
Open
t6s opened 7 months ago
https://github.com/affeldt-aist/infotheo/blob/ee75502025e9fb5b988b025521aabab6f849b2e9/probability/fdist.v#L73 https://github.com/math-comp/analysis/blob/95daf6f73fd773414be3a0878aa0ba0aa6989231/theories/sequences.v#L100
Because of this conflict, these two files cannot be imported at the same time.