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: Dec 20 2025 at 21:32 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: Dec 20 2025 at 21:32 UTC