Zulip Chat Archive

Stream: general

Topic: Simon's "traversable" PR's.

Kevin Buzzard (Jul 27 2018 at 10:41):

What do these do? I can't understand anything :-(

Patrick Massot (Jul 27 2018 at 10:55):

You can have a look at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/type.20class.20traversable but I fear this really CS and software engineering.

Patrick Massot (Jul 27 2018 at 10:55):

I was also planning to ask after Simon will be done with his series of PR

Kevin Buzzard (Jul 27 2018 at 10:58):

Oh so it's nothing to do with the "transportable" proving that if X is a perfectoid space and X equiv Y then Y is a perfectoid space?

Patrick Massot (Jul 27 2018 at 10:58):

I think Simon mentioned a link at some point

Sean Leather (Jul 27 2018 at 11:14):

It's very much CS, though I wouldn't call it software engineering. If you're interested in references, see:
https://hackage.haskell.org/package/base/docs/Data-Traversable.html

Sean Leather (Jul 27 2018 at 11:15):

I believe Simon is setting up infrastructure to simplify expression manipulation and, therefore, tactic writing.

Kevin Buzzard (Jul 27 2018 at 11:28):

Aah thanks!

Simon Hudon (Jul 27 2018 at 12:00):

@Sean Leather that's pretty much it. Plus, I think Lean should be like Haskell as a programming language and traversable should help with that.

@Kevin Buzzard Don't despair, transportable is still under development.

Simon Hudon (Jul 27 2018 at 12:27):

... and so is mono, if people still remember it

Last updated: Dec 20 2023 at 11:08 UTC