computable functions of reals

Stream: maths

[Johan Commelin]

In my "ordinary maths" research I was confronted with the paper "Computable functions of reals" by Tent and Ziegler, which is really funny because:

• Already on the first page it talks about nat-subtraction $\stackrel{\cdot}{-}$.
• It is about computational classes, about which I know nothing
• This felt like stuff which might be pretty Lean-able.
  Here's a link to the paper: http://home.mathematik.uni-freiburg.de/ziegler/preprints/periods.pdf

I'dd like to hear whether others think that these lower-elementary and elementary functions are close to be Leanable or not.

[Patrick Massot]

Noooooooooo!

[Johan Commelin]

Did I say something wrong?

[Patrick Massot]

Johan, please delete that thread before Mario sees it!

[Johan Commelin]

@Mario Carneiro Did you see this thread already, or can I still delete it?

[Patrick Massot]

Remember we still need to be able to handle modules over several base rings

[Patrick Massot]

Now is not a good time to tempt Mario with computability questions

[Johan Commelin]

Right, and there are like 8 PRs on category theory waiting to be merged...

[Patrick Massot]

That too

[Patrick Massot]

Except you, Reid and Scott keep changing everything, and even you don't understand anymore what PR depends on what, and what PR is obsolete

[Patrick Massot]

So I guess Mario and Johannes wisely wait for dust to settle

[Kenny Lau]

what about my 2 PR about ring theory