Zulip Chat Archive

Stream: new members

Topic: generating examples with Lean?

view this post on Zulip Marek (Apr 06 2021 at 04:54):

I am very new to Lean, I am wondering if it is possible to apart from proving a statement is true, to use it to generate an example of a statement. For instance, provided with some definition to perform a search for an instance (or witness) that satisfies that definition. My motivation for it is the following: I am searching for a meta-programming-like tool with high expressiveness that could capture higher order definitions to generate random examples and problems for students. I noticed Lean is used for undergraduate education (ref Xena Project) so it made me curious about it.

view this post on Zulip Scott Morrison (Apr 06 2021 at 05:02):

Perhaps have a look at tactic#slim_check.

view this post on Zulip Marek (Apr 06 2021 at 05:04):

Thank you for quick response! Are you sure this tactic is called slim_check? The only similar entry on the list is type_check.

view this post on Zulip Bryan Gin-ge Chen (Apr 06 2021 at 05:07):

slim_check doesn't have a tactic doc entry (yet). It's documented here and here.

view this post on Zulip Marek (Apr 06 2021 at 05:14):

Amazing! Thank you!

Last updated: May 13 2021 at 22:15 UTC