amusing

Stream: lean4

[Julian Berman]

Forgive me, I can't resist finding the fact that this compiles without sorrys or complaints amusing :D

namespace «

theorem fermats_last_theorem
  {a b c n : Nat}
  (apos : a > 0)
  (bpos : b > 0)
  (cpos : c > 0)
  (h : a^n + b^n = c^n)
  : n = 2 := by
    trivial

»

[Leonardo de Moura]

I find this kind of message very distracting. It is unclear what its purpose is.
Are you requesting we change how escaped identifiers behave?
Or, do you want us to check unclosed namespace/sections when the file ends?
Or, are you just trying to be funny?

[Julian Berman]

@Leonardo de Moura apologies, I suspected it was better for New Members or some other less important place since yes it was mostly not meant to have any action associated with it --

but perhaps now that I've said it here and noticed lean 3 does not allow these escaped identifiers with as much liberty, maybe not allowing newlines in escaped identifiers is a good way to restrict them?

[Gabriel Ebner]

I don't see a problem here. The French quotes are even highlighted correctly in vscode. If you don't like French quotes, you can also use comments:

section /-
theorem equal_two_of_pow_add_pow_eq_pow : ....
-/

[Gabriel Ebner]

BTW, there's a long tradition of hiding Fermat's last theorem in comments. For example, this post on coq-club soon celebrates its twelfth birthday:
https://sympa.inria.fr/sympa/arc/coq-club/2009-04/msg00006.html

[Mario Carneiro]

I think that tradition dates back to Fermat himself