Zulip Chat Archive

Stream: new members

Topic: Parsing goal/context


view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 07 2020 at 16:09):

Clicking on the goal will show you the head symbol.

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Aug 07 2020 at 16:13):

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

view this post on Zulip Pim Spelier (Aug 07 2020 at 16:35):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Utensil Song (Aug 08 2020 at 09:37):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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