noncomputable detection

Stream: general

[Kevin Kappelmann]

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]

maybe run lean on something like

import myfile
def a := mydefinition

and see if you get an error

[Kevin Kappelmann]

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

[Kevin Kappelmann]

@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.