structure fields of a parent structure are not resolved correctly

[kim-em]

See https://github.com/leanprover-community/mathlib3port/blob/948275e/Mathbin/CategoryTheory/Category/Basic.lean#L74 for an example. The appearances of hom here should be Hom (referring to Quiver.Hom).

Presumably when mathport is looking up these identifiers it is not looking in the Quiver namespace, so we will need to add parent structures at the appropriate point in resolution.

[gebner]

The same issue also appears in dot-notation: https://github.com/leanprover-community/mathlib3port/blob/9b3a383ce98f5dce5e1b922c8b1614a9befa909a/Mathbin/Topology/ContinuousFunction/Bounded.lean#L42

instance : CoeFun (α →ᵇ β) fun _ => α → β :=
  ⟨fun f => f.to_fun⟩

[gebner]

The coeFun issue I mentioned is fixed now. Scott's hom issue is still present though:

class category_struct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
  id : ∀ X : obj, hom X X
  comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
-- ...
class category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where

(There's also the incorrect category_struct and category names here.)

[dselsam]

• I thought https://github.com/leanprover-community/mathport/commit/61b4659b7bcbf2c61b09db8370487b6f78403701 would solve the hom issue -- I even had a self-contained file that I thought mimic-ed the setup that the commit fixed.

• class category_struct and class category is a different issue, since presumably the parser doesn't resolve those names. We should just auto-Pascal the identifiers for all inductive type declarations.

[dselsam]

It looks like the parser doesn't actually resolve the hom at all, because the parser does not know it is in the namespace of the extends when it parses the result type.

[gebner]

class category_struct and class category is a different issue, since presumably the parser doesn't resolve those names. We should just auto-Pascal the identifiers for all inductive type declarations.

This was easy to fix, since we can compute the Lean 3 name by namespace name ++ declaration name and then rename it like a constant. #110