Zulip Chat Archive

Stream: lean4

Topic: amusing


view this post on Zulip Julian Berman (Mar 08 2021 at 19:58):

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

»

view this post on Zulip Leonardo de Moura (Mar 08 2021 at 20:25):

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?

view this post on Zulip Julian Berman (Mar 08 2021 at 20:28):

@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?

view this post on Zulip Gabriel Ebner (Mar 08 2021 at 20:32):

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 : ....
-/

view this post on Zulip Gabriel Ebner (Mar 08 2021 at 20:36):

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

view this post on Zulip Mario Carneiro (Mar 09 2021 at 05:17):

I think that tradition dates back to Fermat himself


Last updated: May 18 2021 at 23:14 UTC