Zulip Chat Archive
Stream: lean4
Topic: by apply_instance
Kenny Lau (Jan 05 2021 at 21:05):
What's the Lean 4 equivalent of by apply_instance?
Bryan Gin-ge Chen (Jan 05 2021 at 21:07):
There's inferInstance (which I haven't tried) and also a #synth command (which I've tried once).
Kenny Lau (Jan 05 2021 at 21:10):
Thanks, #synth works
Last updated: Dec 20 2023 at 11:08 UTC