state doesn't work

[fpvandoorn]

The state tactic doesn't print any output in the online version:

example : bool := by state; exact bool.tt

[soonhokong]

It's because --flycheck option doesn't change the output for the state tactic (while we expect that the use of --flycheck option wraps the output so that we can extract the output). For example, this is what we have for now:

$lean test.lean
test.lean:1:21: proof state

⊢ bool

$ lean test.lean --flycheck
test.lean:1:21: proof state

⊢ bool

Leo is on vacation now. I'll check what I can do with this.

[fpvandoorn]

Leo is on vacation now. I'll check what I can do with this.

This is not at all high priority, so don't worry too much if this is something Leo can do better.