Custom prefixes

Stream: lean-gptf

[Jesse Michael Han]

New feature: you can now call gptf {pfx := $TAC} to force gptf to create a prediction using a certain tactic! For example, you can do gptf {pfx := "rw"} (resp. apply, exact, simp...). It's really interesting seeing what it thinks are good simp lemmas and what is a good idea to try for exact.

[Jesse Michael Han]

You can now also pass an arbitrary postprocessing function, which lets you e.g. ask the model to predict rw hypotheses, then use them for [smt] eblast_using .... This example is now available as neuro_eblast.