Type representing continuous functions with different approximation types on compact domain

[fbrausse]

Suppose one constructs an e.g. linear function f:x\mapsto ax+b with a, b of type REAL and wants to approximate f on a real interval [l,u] up to precision p as another linear function g:x\mapsto cx+d, that is, c,d should now be of type DYADIC with the property

forall x in [l,u] : |f(x) - g(x)| < 2^p

This could be generalized to polynomials or rational functions and may be a first step towards piecewise approximations on a larger domain.