Commit 2023-04-18 12:01 2d98ae59

feat: propose, a forwards-reasoning analogue of library_search. (#2898)

• propose using a, b, c tries to find a lemma which makes use of each of the local hypotheses a, b, c, and reports any results via trace messages.
• propose : h using a, b, c only returns lemmas whose type matches h (which may contain _).
• propose! using a, b, c will also call have to add results to the local goal state. propose should not be left in proofs; it is a search tool, like library_search.