generating examples with Lean?

Stream: new members

[Marek]

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.

[Scott Morrison]

Perhaps have a look at tactic#slim_check.

[Marek]

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

[Bryan Gin-ge Chen]

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

[Marek]

Amazing! Thank you!