infotheo
infotheo copied to clipboard
Notations for random variables conflict between infotheo and mathcomp-analysis
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 }").