search

affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

Notations for random variables conflict between infotheo and mathcomp-analysis #114

Open t6s opened 7 months ago

t6s commented 7 months ago

The following expression fails to be parsed after importing both proba.v (infotheo) and probability.v (mathcomp-analysis):

Local Open Scope form_scope.
Variables (d : measure_display) (T : measurableType d) (R : realType) (P : probability T R).
Variable (X : {RV P >-> R}).

>>> Error: Syntax error: '->' expected after [term] (in [term]).

A similar reserved notation in proba.v seems to be confusing the parser:

Reserved Notation "{ 'RV' d -> T }" (at level 0, d, T at next level,
  format "{ 'RV'  d  ->  T }").