Different renaming in binport vs. synport

[gebner]

Apparently it's CategoryTheory.Bundled in binport, but CategoryTheory.bundled in synport.

-- Mathbin/CategoryTheory/ConcreteCategory/Bundled.lean
structure bundled (c : Type u → Type v) : Type max (u + 1) v where
  α : Type u
  str : c α := by
    run_tac
      tactic.apply_instance

-- Mathbin/MeasureTheory/Category/Meas.lean
def Meas : Type (u + 1) :=
  bundled MeasurableSpace -- ■ unknown identifier 'bundled'

[dselsam]

This issue is related to #58. The following line in synport is problematic: https://github.com/leanprover-community/mathport/blob/master/Mathport/Syntax/Translate/Basic.lean#L163. We need to take the namespace and open declarations into account somehow. It may not be easy in general to infer what the name would have resolved to in Lean3, but in the common case checking the binported term against the possible capitalizations will return only one compatible option. We can do the same (heuristic) trick for field names as well.

[gebner]

It may not be easy in general to infer what the name would have resolved to in Lean3

We could store the resolved name in the AST files (it's already known at parsing time in most cases).