binders position info

Stream: lean4

[Patrick Massot]

When using docs4#Lean.Environment.find? to retrieve a theorem statement, is there way to know what was left of the colon and what was right of the colon?

[Jannis Limperg]

I'm pretty sure this information is not preserved.

[Patrick Massot]

Thanks for this answer. I'm a bit sad but I'll work around this.

[Mario Carneiro]

why do you need this? It was erased as a relevant distinction

[Patrick Massot]

Relevant for what?

[Patrick Massot]

I'm returning to working on the game server (aiming in particular for the natural number game in Lean 4).

[Eric Wieser]

Why does the game server need to know what was before or after the colon?

[Patrick Massot]

In some levels you want people to use intro and in other levels you don't

[Eric Wieser]

Is the idea to not have to do the source-replacement trick that I think the lean3 game-maker does?

[Patrick Massot]

I don't know what the source-replacement trick, but there won't be anything in common with what game-maker does.

[Mario Carneiro]

could you give an example?

[Mario Carneiro]

I would expect the decision of whether to use intro or not to depend on the state of the proof

[Patrick Massot]

But Lean doesn't remember the state of the proof at the beginning of a theorem, that's my problem.

[Mario Carneiro]

you could override by or def to record the information you are interested in

[Eric Wieser]

To what extent could something like

example (before_the_colon : P) : Q := by start_the_game_already

work for the server you're building? Couldstart_the_game_alreadystart the server itself, or at least add the goal state to the queue of games to play?