infotheo icon indicating copy to clipboard operation
infotheo copied to clipboard

Notations for random variables conflict between infotheo and mathcomp-analysis

Open t6s opened this issue 11 months ago • 0 comments

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 }").

t6s avatar Mar 11 '24 15:03 t6s