Zulip Chat Archive

Stream: triage

Topic: issue #1922: Intuitionistic versions of `finish` use clas...


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jan 19 2021 at 14:49):

This bot is very polite, it doesn't ask "Was this issue ever relevant?"

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 19 2021 at 14:51):

I know... I'm joking.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 19 2021 at 14:53):

I urged him to ask questions here, rather than asking me...

view this post on Zulip Kevin Buzzard (Jan 19 2021 at 14:54):

He told me that using LEM was cheating.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 19 2021 at 14:57):

Did you also tell him computer scientists should become reasonable and drop that ridiculous lambda notation?

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Mar 15 2021 at 14:28):

This was addressed by #5897 so I've closed it.


Last updated: May 18 2021 at 23:14 UTC