Use of `have' in lean4game

Stream: general

[Ma, Jia-Jun]

I am trying to develop a game. But failed to utilize `have' to introduce a new intermediate goal in the game.

In the web interface, I tried

have hh : ∀ a:G, a⁻¹ = a

The error message says :

unexpected end of input; expected '|'

Any suggestions?

[Ma, Jia-Jun]

Ma, Jia-Jun said:
I tried again, and magically it worked.

I am trying to develop a game. But failed to utilize `have' to introduce a new intermediate goal in the game.

In the web interface, I tried

have hh : ∀ a:G, a⁻¹ = a

[Jon Eugster]

import mathlib's have, or copy-paste its definition into your game.

I think it's import Mathlib.Tactic.Have or something