Stream: math-comp analysis

Topic: Searching for a lemma


view this post on Zulip Marie Kerjean (May 15 2020 at 11:50):

I'm creating a new topic for naming/lemmas research, is that ok ?

view this post on Zulip Marie Kerjean (May 15 2020 at 11:50):

(deleted)

view this post on Zulip Cyril Cohen (May 15 2020 at 12:12):

yes always create new topics for new stuff, it's the recommanded usage!

view this post on Zulip Cyril Cohen (May 15 2020 at 12:12):

What do you want to say though?

view this post on Zulip Marie Kerjean (May 15 2020 at 12:42):

I was looking for the new name of flim_trans and for near_eq_cvg. Found them now :)

view this post on Zulip Reynald Affeldt (May 15 2020 at 13:02):

Indeed, they were part of the last big renaming

view this post on Zulip Marie Kerjean (May 15 2020 at 13:04):

That was PR199 right ? Is the renaming described precisely somewhere, with flim -> cvg ?

view this post on Zulip Marie Kerjean (May 15 2020 at 13:07):

I am struggling to adapt my fork of holomorphy.v, which dates back to february.

view this post on Zulip Reynald Affeldt (May 15 2020 at 13:18):

I don't think there is much more than the PR and its conversation

view this post on Zulip Reynald Affeldt (May 15 2020 at 13:18):

but I don't understand: I think I did it on the branch cauchy_etoile

view this post on Zulip Cyril Cohen (May 15 2020 at 13:18):

mkerjean said:

That was PR199 right ? Is the renaming described precisely somewhere, with flim -> cvg ?

affeldt-aist said:

I don't think there is much more than the PR and its conversation

yes there is

view this post on Zulip Cyril Cohen (May 15 2020 at 13:19):

I provide a sed script for the migration

view this post on Zulip Cyril Cohen (May 15 2020 at 13:19):

math-comp/analysis#193

view this post on Zulip Cyril Cohen (May 15 2020 at 13:20):

If you have trouble using it, I can do the migration for you if you first rebase yourself on top of the commit math-comp/analysis#283b4330aa4327640c6e6a499c861ebc714ddd18

view this post on Zulip Reynald Affeldt (May 15 2020 at 13:25):

I don't think there is much more than the PR and its conversation

yes there is

Indeed, my mistake, I forgot: the file is pr193.sed in the directory etc.


Last updated: Aug 11 2022 at 01:03 UTC