mathport align issue?

Stream: mathlib4

[Arien Malec]

I noted in a port I just did that forall_and_distrib needed to be manually aligned from Mathlib.Logic.Basic to forall_and in Std.Logc despite the align statement:

#align forall_and_distrib forall_and

Is there something that needs fixing either in the align statement or in mathport?

[Mario Carneiro]

what was the situation?

[Johan Commelin]

@Arien Malec Was it in a situation like simp [forall_and_distrib]?

[Johan Commelin]

Identifiers that are part of tactic invocations are currently not really ported by mathport. But hopefully this will change soon.

[Arien Malec]

After manual aligning (!4#1990)

refine'
    mem_finsupp_iff.trans
      (forall_and.symm.trans <|
        forall_congr' fun i =>
          ⟨fun h => _, fun h =>
            ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi _, fun _ => h⟩⟩)

[Johan Commelin]

@Reid Barton do you think this is part of the same issue? I guess refine' is a bit different from rw and simp...

[Reid Barton]

it seems to have something to do with forall_and_distrib.foo

[Reid Barton]

Maybe combined with the fact that it is in a tactic

[Reid Barton]

Perhaps the parser sees the whole forall_and_distrib.symm.trans as a single ident

[Mario Carneiro]

Reid Barton said:

Perhaps the parser sees the whole forall_and_distrib.symm.trans as a single ident

I believe this is the issue. if it was not in a tactic then it would be resolved on the spot but here it is being preserved as a pexpr and it won't be resolved until the tactic is run. Depending on what local variables are in scope when it is run that ident might get split up in different ways at elaboration time