Commit 2021-06-02 10:33 b91cdb91

refactor(data/nnreal): rename nnreal.of_real to real.to_nnreal (#7750) I am in the middle of a project involving reals, nnreals, ennreals and ereals. There is a maze of coercions and maps between the 4 of them, with completely incoherent naming scheme (do you think that measurable.nnreal_coe is speaking of the coercion from nnreal to real or to ennreal, or of a coercion into nnreal? currently, it's for the coercion from nnreal to real, and the analogous lemma for the coercion from nnreal to ennreal is called measurable.ennreal_coe!). I'd like to normalize all this to have something coherent:

• maps are defined from a type to another one, to be able to use dot notation.
• when there are coercions, all lemmas should be formulated in terms of the coercion, and not of the explicit map
• when there is an ambiguity, lemmas on coercions should mention both the source and the target (like in measurable.coe_nnreal_real, say). The PR is one first step in this direction, renaming nnreal.of_real to real.to_nnreal (which makes it possible to use dot notation).