Zulip Chat Archive

Stream: general

Topic: noncomputable detection


view this post on Zulip Kevin Kappelmann (Jun 18 2020 at 19:19):

Hi all, given some lean file, I want to check if a certain definition is computable. Is there a good way to do this using the lean compiler or leanchecker?

view this post on Zulip Reid Barton (Jun 18 2020 at 19:26):

maybe run lean on something like

import myfile
def a := mydefinition

and see if you get an error

view this post on Zulip Kevin Kappelmann (Jun 18 2020 at 19:36):

oh, it does indeed - I thought it won't be that simple for some reason, haha. thank you! :)

view this post on Zulip Kevin Kappelmann (Jun 18 2020 at 20:04):

@Donald Sebastian Leung not sure if you already have some katas with computability restrictions, but that pattern seems to work. You were mentioning that you would like these kind of checks too a while ago.


Last updated: May 08 2021 at 04:14 UTC