Stream: new members
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.
Scott Morrison (Apr 06 2021 at 05:02):
Perhaps have a look at tactic#slim_check.
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
Bryan Gin-ge Chen (Apr 06 2021 at 05:07):
Marek (Apr 06 2021 at 05:14):
Amazing! Thank you!
Last updated: May 13 2021 at 22:15 UTC