returning true or false

Stream: new members

[ebp]

Hi all!

I am currently discovering Lean v.3, and enjoying it really at the moment. I am looking for a way to let Lean return "true" or "false", given a hypothetical proof of an "example" . For example, if I have the standard proof of p -> p, in a file prop.lean, running lean prop.lean in the terminal just stays silent, showing that the proof does not yield any problem. If I remove the last sentence, Lean tells me that there are unsolved goals. However, I want to simplify the latter to the return of "False", and the first to the return of "True". Can anyone hint me towards a solution to this?

[ebp]

In fact, this question generalizes to the question on how to decide what output lean prop.lean gives, and how to influence this output.

[Jannis Limperg]

I don't think you can easily influence Lean's output from within Lean. However, you can write a shell script that checks the exit code of lean prop.lean and prints "True" if 0, "False" otherwise.

However, this feels a bit like an #xy problem. What are you trying to do that makes you want this behaviour?

[ebp]

Ultimately I would like to be able to influence the output in order to implement Lean in a larger "infrastructure". I suspect it to be the case that doing this in Lean itself would give me more "hold" on this than doing it in the shell itself.

I thought that just like you are able to print something like "Hello world" from a script, it would be possible to print other things depending on the status of a proof of an example.

[Jannis Limperg]

I see. Afaik Lean 3 doesn't provide this capability, so the shell is your best bet (or forking Lean). In Lean 4 it might be possible to override the elaboration function for commands like example from within the system. But this is probably not so easy either.

[ebp]

Ah, allright. Thanks! I will work with shell scripts for now, but would love to hear if anyone has an alternative idea!

[Julian Berman]

I'd agree nothing seems like it could be easier than lean foo.lean && echo "True" || echo "False" but if you have other constraints that make you not want to do that you probably should share them.