The following PR to MathComp-Analysis (https://github.com/math-comp/analysis/pull/1256, this is actually wip)
seems to illustrate a potential improvement to HB. Concretely, we tried to generalize the structure of measurable
functions (from a realType codomain to any measurableType) and then equipping the constant function with both
the type of measurable functions and the type of simple functions (i.e., with codomain realType) caused HB to
complain that constant functions aren't all simple functions; we avoided the problem so far by restricting ourselves
to real-valued functions. We found a kludge that we are in the process of experimenting.
The following PR to MathComp-Analysis (https://github.com/math-comp/analysis/pull/1256, this is actually wip) seems to illustrate a potential improvement to HB. Concretely, we tried to generalize the structure of measurable functions (from a realType codomain to any measurableType) and then equipping the constant function with both the type of measurable functions and the type of simple functions (i.e., with codomain realType) caused HB to complain that constant functions aren't all simple functions; we avoided the problem so far by restricting ourselves to real-valued functions. We found a kludge that we are in the process of experimenting.
@t6s @hoheinzollern