Zulip Chat Archive

Stream: general

Topic: noncomputable detection

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?

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

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! :)

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: Aug 03 2023 at 10:10 UTC