Zulip Chat Archive
Stream: lean4
Topic: mk_instance
Chris Hughes (Aug 13 2021 at 12:52):
I couldn't find anything in Lean 4 that does what mk_instance does in Lean 3. What should I use for this?
Last updated: Feb 28 2026 at 14:05 UTC
I couldn't find anything in Lean 4 that does what mk_instance does in Lean 3. What should I use for this?
Last updated: Feb 28 2026 at 14:05 UTC