When a non-fully-qualified name occurred directly as one of:
the entire body of a definition/theorem
an argument to notation (e.g., a in a + 1)
mathport did not keep track of the pexpr containing the fully-qualified name, and as a result, would not in general translate it to the aligned Lean 4 version. Fix this by passing along the pexpr data.
digama0
commented
1 year ago
When a non-fully-qualified name occurred directly as one of:
aina + 1)mathport did not keep track of the pexpr containing the fully-qualified name, and as a result, would not in general translate it to the aligned Lean 4 version. Fix this by passing along the pexpr data.