Zulip Chat Archive
Stream: general
Topic: test
Sebastian Ullrich (Feb 26 2018 at 16:07):
meta def f := by sorry
Sebastian Ullrich (Feb 26 2018 at 16:12):
Patrick Massot (Feb 26 2018 at 16:22):
Did you find a way to tell Zulip that Lean is the default language for code blocks here?
Patrick Massot (Feb 26 2018 at 16:22):
Or do we have to specify lean after the opening triple backquote?
Last updated: May 02 2025 at 03:31 UTC