Stream: General

Topic: Feeding searched lemmas to Sledgehammer

view this post on Zulip Gergely Buday (Aug 22 2024 at 08:58):

Is there a syntax to feed the found theorems of a find_theorems call to Sledgehammer?

lemma "foo" using >> find_theorems " search expression" << sledgehammer

?

view this post on Zulip Gergely Buday (Aug 22 2024 at 09:37):

Probably a way to suppress theorems output and display only theorem names, with only spaces between them?

Last updated: Feb 28 2025 at 08:24 UTC