## Stream: new members

### Topic: Parsing goal/context

#### Pim Spelier (Aug 07 2020 at 16:08):

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 (Aug 07 2020 at 16:09):

Clicking on the goal will show you the head symbol.

#### Pim Spelier (Aug 07 2020 at 16:13):

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

#### Patrick Massot (Aug 07 2020 at 16:13):

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

#### Pim Spelier (Aug 07 2020 at 16:35):

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

#### Utensil Song (Aug 08 2020 at 08:12):

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

#### Pim Spelier (Aug 08 2020 at 09:28):

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 (Aug 08 2020 at 09:37):

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 (Aug 08 2020 at 09:37):

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

#### Pim Spelier (Aug 08 2020 at 09:40):

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

#### Pim Spelier (Aug 08 2020 at 09:42):

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 (Aug 08 2020 at 09:42):

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 (Aug 08 2020 at 09:50):

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 (Aug 08 2020 at 16:41):

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

Last updated: May 12 2021 at 04:19 UTC