Is it possible to query the goal texts in a tactic state?

leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.

54 stars 13 forks source link

Is it possible to query the goal texts in a tactic state? #19

Closed UltimatePea closed 7 months ago

UltimatePea commented 7 months ago

From README it seems that the only data associated with a proof state is its goal type. Is it possible to query premises of a tactic state?

semorrison commented 7 months ago

Yes, all hypotheses are included in the goal states, appearing before the turnstile symbol ⊢.

The examples in the README don't have hypotheses!

UltimatePea commented 7 months ago

Thank you very much for the clarification!

I see that the goal text does not have the new line ("\n") character, and all hypothesis seems to be stacked together. Is it possible to request for the exact goal state?

semorrison commented 7 months ago

@UltimatePea, thank you for pointing this out! That was definitely an oversight, and is now fixed.