Zulip Chat Archive
Stream: lean4
Topic: unterminated comments
Jason Gross (Mar 11 2021 at 19:37):
Is
#print Nat
/-
supposed to error on the N with expected 'axioms', identifier or string literal? This seems pretty confusing...
Sebastian Ullrich (Mar 15 2021 at 17:53):
Fixed in https://github.com/leanprover/lean4/pull/347
Jason Gross (Mar 15 2021 at 17:59):
Thanks!
Last updated: May 02 2025 at 03:31 UTC