How to break lines

Stream: general

[Miguel Marco]

I am trying to wrote a tactic that behaves like field_simp, but also uses cancelation in denominators (adding the corresponding hypothesis to be proved as new goals). It is basically a sequence of rewrites:

syntax "unify_denoms" (location)? : tactic

macro_rules
| `(tactic | unify_denoms $[at $location]?) => `(tactic |( field_simp $[at $location]?;  repeat (first | rw [← one_div] $[at $location]? | rw [div_add_div] $[at $location]?| rw [div_sub_div] $[at $location]?| rw [add_div'] $[at $location]?| rw [div_add'] $[at $location]?| rw [add_sub'] $[at $location]?| rw [sub_div'] $[at $location]? | rw [mul_div_mul_right] $[at $location]? | rw [mul_div_mul_left] $[at $location]?)))

as you can see, it results in a very long line, but if i try to split it, it gives errors. So I have two questions:

• Is there a way to break the line so it looks better, but Lean still considers it as a single line in terms of syntax?
• Is there a more elegant (or better in a general sense) to do this kind of thing?

[Alex J. Best]

#mwe? I would expect that you could break that in many places without errors

[Shreyas Srinivas]

Extra brackets

[Shreyas Srinivas]

You need extra brackets starting after (tactic|

[Alex J. Best]

One other thing to do is use $loc instead of $location seeing as you have it 5 times

[Miguel Marco]

Alex J. Best said:

#mwe? I would expect that you could break that in many places without errors

This:

syntax "unify_denoms" (location)? : tactic

macro_rules
| `(tactic | unify_denoms $[at $loc]?) => `(tactic | ( field_simp $[at $loc]?;  repeat (first | (rw [← one_div] $[at $loc]?) |
 (rw [div_add_div] $[at $loc]?) | (rw [div_sub_div] $[at $loc]? ))))

gives me an error: expected ')'. It highlights the first | in the last line.

[Shreyas Srinivas]

This is not an mwe since there is no syntax category by the name location in this example

[Miguel Marco]

Changing loc to location has the same behaviour.

[Alex J. Best]

No I just mean that it will make your line shorter and easier to read

[Shreyas Srinivas]

I disagree with Alex since I am a fan of descriptive names, but it will really help us if you have an example where everything else is in place

[Kevin Buzzard]

@Miguel Marco your code gives me unknown parser declaration/category/alias 'location'. Can you post a #mwe ? Click on the link if you don't know what I'm talking about.

[Alex J. Best]

import Mathlib

open Lean Meta Elab Tactic Parser Tactic
syntax "unify_denoms" (location)? : tactic

macro_rules
| `(tactic | unify_denoms $[at $loc]?) => `(tacticSeq |
  field_simp $[at $loc]?
  repeat (first
    | (rw [← one_div] $[at $loc]?)
    | (rw [div_add_div] $[at $loc]?)
    | (rw [div_sub_div] $[at $loc]?)))

[Alex J. Best]

Shreyas Srinivas said:

I disagree with Alex since I am a fan of descriptive names, but it will really help us if you have an example where everything else is in place

In general I agree but $loc is already quite common in the library, so anybody reading it probably knows what it means

[Miguel Marco]

Alex J. Best said:

No I just mean that it will make your line shorter and easier to read

Yes, I get that. I just wanted to point that that change is not the culprit. So the mwe would be:

open Lean.Parser.Tactic

syntax "unify_denoms" (location)? : tactic

macro_rules
| `(tactic | unify_denoms $[at $location]?) => `(tactic | (( field_simp $[at $location]?;  repeat (first | (rw [← one_div] $[at $location]? |
 rw [div_add_div] $[at $location]? | rw [div_sub_div] $[at $location]? ))))

[Kevin Buzzard]

unknown tactic

[Alex J. Best]

I've already worked out and posted the correct opens above.

[Shreyas Srinivas]

1. That is not an #mwe since the syntax line has an unknown syntax category, which leads to it not being registered, ergo unknown tactic error on the macro
2. The below also works

import Mathlib

open Lean Meta Elab Tactic Parser Tactic
syntax "unify_denoms" (location)? : tactic

macro_rules
| `(tactic | unify_denoms $[at $loc]?) => `(tactic |(
  field_simp $[at $loc]?
  repeat (first
    | (rw [← one_div] $[at $loc]?)
    | (rw [div_add_div] $[at $loc]?)
    | (rw [div_sub_div] $[at $loc]?))))

[Kevin Buzzard]

Alex has answered your question, but I'm just trying to make the point that you should check your posts by cutting and pasting into a new file. It makes everyone else's life easier.

[Miguel Marco]

Thanks everybody. It works.