Zulip Chat Archive
Stream: triage
Topic: issue #1922: Intuitionistic versions of `finish` use clas...
Random Issue Bot (Nov 20 2020 at 14:19):
Today I chose issue 1922 for discussion!
Intuitionistic versions of finish use classical axioms
Created by @Rob Lewis (@robertylewis) on 2020-01-28
Labels: bug, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Rob Lewis (Nov 20 2020 at 15:35):
This won't be fixed in Lean 3 unless someone decides they care about constructive proof search enough to work on it. The issue is still open as a warning.
Random Issue Bot (Dec 08 2020 at 14:24):
Today I chose issue 1922 for discussion!
Intuitionistic versions of finish use classical axioms
Created by @Rob Lewis (@robertylewis) on 2020-01-28
Labels: bug, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 19 2021 at 14:46):
Today I chose issue 1922 for discussion!
Intuitionistic versions of finish use classical axioms
Created by @Rob Lewis (@robertylewis) on 2020-01-28
Labels: bug, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Patrick Massot (Jan 19 2021 at 14:49):
This bot is very polite, it doesn't ask "Was this issue ever relevant?"
Kevin Buzzard (Jan 19 2021 at 14:50):
It certainly wasn't to you! But I was talking about this sort of thing with some guy called Philip Wadler yesterday (he asked a question after a talk I gave at a crypto company) and he certainly seemed to think it was.
Patrick Massot (Jan 19 2021 at 14:51):
I know... I'm joking.
Kevin Buzzard (Jan 19 2021 at 14:51):
I'm not sure I gave a very good answer to Wadler, unfortunately. I also mentioned that "apparently Lean 4 is faster than Haskell" and he got very animated.
Kevin Buzzard (Jan 19 2021 at 14:53):
I urged him to ask questions here, rather than asking me...
Kevin Buzzard (Jan 19 2021 at 14:54):
He told me that using LEM was cheating.
Patrick Massot (Jan 19 2021 at 14:54):
We should gather once and for all a list of names we should be aware of before giving talks in front of computer sciency audiences.
Kevin Buzzard (Jan 19 2021 at 14:56):
Seriously, I do hope that Wadler comes and asks his questions. I told him that unfortunately most of our maths library would not be of much use to him, but I also suggested that he probably wasn't interested in most of our maths library anyway.
Patrick Massot (Jan 19 2021 at 14:57):
Did you also tell him computer scientists should become reasonable and drop that ridiculous lambda notation?
Random Issue Bot (Mar 15 2021 at 14:26):
Today I chose issue 1922 for discussion!
Intuitionistic versions of finish use classical axioms
Created by @Rob Lewis (@robertylewis) on 2020-01-28
Labels: bug, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Bryan Gin-ge Chen (Mar 15 2021 at 14:28):
This was addressed by #5897 so I've closed it.
Last updated: Dec 20 2023 at 11:08 UTC