Allowing Calc for lean game server to use?

Stream: new members

[Qi Wen Wei]

Hey! I currently have a lean game server setup as a side project. However I can't seem to be able to enter calc mode within the client.

Screenshot 2024-11-16 150624.png

Since it is not a tactic and part of lean itself, is there any way to enable it for the game?

It works fine in visual studios though:
t2.png

Thanks for the help!

[Kevin Buzzard]

Did you try switching the button on the front page of the game to the "lawless" mode? I forgot what it's called, but it's the bottom one of the three options (edit: it's called "rules: none")

[Kevin Buzzard]

Otherwise you'll have to explicitly enable the calc tactic in your code

[Qi Wen Wei]

Kevin Buzzard said:

Did you try switching the button on the front page of the game to the "lawless" mode? I forgot what it's called, but it's the bottom one of the three options

I don't see the "lawless" mode button.
T1.png

[Qi Wen Wei]

Kevin Buzzard said:

Otherwise you'll have to explicitly enable the calc tactic in your code

Do you happen to know where to do this? Also, I thought calc wasn't a tactic?

[Kevin Buzzard]

"Rules: none" is what I mean.

[Qi Wen Wei]

Oh, it works now. I guess I should have played around a bit more before asking.

Thanks for all the help.

[Kevin Buzzard]

Lines like this are what enables tactics to be used in "regular" mode. Also look above that line for how I set up the docstring for the tactic.

[Kevin Buzzard]

I think calc is a tactic, as well as being a "mode". If it were not then by calc... would fail. Probably if you know what you're doing (and I don't) then it's easy to verify this (that sort of thing is all a bit meta for me in Lean 4).

Yeah, if I write

example : 2 + 2 = 4 := by
  calc 2 + 2 = 2 + 2 := by rfl
       _     = 4     := by rfl

and right-click on calc I can jump to definition and whilst I don't really understand the code, I think it says that that particular calc is a tactic.

[Kevin Buzzard]

And if you remove the by then you jump somewhere completely different. calc really must be two things.

[Kevin Buzzard]

here is the discussion in the docs about NewTactic by the way.