Parsing goal/context

Stream: new members

[Pim Spelier]

Hi,
Sometimes I have trouble parsing the local context or a goal; if my goal is 5 lines for example, I can't automatically parse whether it's an equality, an iff statement, a forall statement or something else. Is there a nice way to indent this in the infoview so I can immediately see this? I know I can copy the state to a comment, and then it'll show it nice and parsable, but I'd prefer if it were possible directly in the infoview itself somehow.

[Patrick Massot]

Clicking on the goal will show you the head symbol.

[Pim Spelier]

Only if you click on the right part, right? (E.g.., on the =-symbol if it's an equality)

[Patrick Massot]

You can move your mouse over the goal until everything gets highlighted

[Pim Spelier]

So there's no automatic indentation? Then I'll follow your approach, thanks!

[Utensil Song]

@Pim Spelier Do you have an example of such a long goal? So everyone could have an intuitive idea about the indentation.

[Pim Spelier]

An example:

⊢ ∀ (a_1 : turing.TM2.cfg tr.Γ tr.Λ tr.σ), a_1 ∈ roption.of_option (↑(init_list tr.k₀ tr.Γ tr.Λ tr.σ (_.mpr (ea.to_encoding.encode a))).bind (λ (c : turing.TM2.cfg tr.Γ tr.Λ tr.σ), option.rec none (λ (val : tr.Λ), some {l := none tr.Λ, var := c.var, stk := c.stk}) c.l)) ↔ a_1 ∈ roption.map (halt_list tr.k₁ tr.Γ tr.Λ tr.σ) (_.mpr (roption.some (ea.to_encoding.encode a)))

which, when "copy state to comment"'ed, gives

⊢ ∀ (a_1 : turing.TM2.cfg tr.Γ tr.Λ tr.σ),
    a_1 ∈
        roption.of_option
          (↑(init_list tr.k₀ tr.Γ tr.Λ tr.σ (_.mpr (ea.to_encoding.encode a))).bind
             (λ (c : turing.TM2.cfg tr.Γ tr.Λ tr.σ),
                option.rec none (λ (val : tr.Λ), some {l := none tr.Λ, var := c.var, stk := c.stk}) c.l)) ↔
      a_1 ∈ roption.map (halt_list tr.k₁ tr.Γ tr.Λ tr.σ) (_.mpr (roption.some (ea.to_encoding.encode a)))

making it clear that it's stating that for all a, a certain iff-statement hold. With Patrick's tip, you can easily see that it's a forall statement if you start at the beginning, but to see that it's a forall a, ... ↔ ... statement, you'd need to mouse over exactly the right character.
It's not really that big of a problem, the "copy state to comment"'ing does work, but I was just wondering if it's possible somehow (clearly there is code for indentation somewhere)

[Utensil Song]

Take a look at the code, vscode-lean doesn't seem to do indentation in "copy state to comment", it just put /- -/ around the text. This could be the difference between plain text mode and widget mode, which indicates this could be a widget improvement?

[Utensil Song]

Can you try switching back to plain text mode? Do you see the indentation after that?

[Pim Spelier]

That works, thanks! Then it misses the widget benefits, but I can just switch back and forth as need be for now.

[Pim Spelier]

Just curious: does that mean the widget actively removes the indentation? Or does the indentation just not survive the parsing by the widget?

[Utensil Song]

But the indentation in the pasted comment is also not showing that it's a ∀ a, ... ↔ ... statement either. Maybe there could be a smart indentation using a top-down approach for widget view?

[Pim Spelier]

The indentation in the comment is kinda showing it's a ∀ a, ... ↔ ... statement, but you do have to know you have to look at the end of the 6th (first to last) line to see the relation between the block starting at the second line and the last line.

[Kevin Buzzard]

If you set_option pp.all true and then turn widgets off you get an output which has correct indentation spacing but I've found that using the widget functionality is easier in practice