Gabriel Ebner

I tried to do this using ``mathport_rules | `(coe) => `((↑))``, but this is trickier than I'd thought at first. The issue is that the `coe` constant is represented in...

The same issue also appears in dot-notation: https://github.com/leanprover-community/mathlib3port/blob/9b3a383ce98f5dce5e1b922c8b1614a9befa909a/Mathbin/Topology/ContinuousFunction/Bounded.lean#L42 ```lean instance : CoeFun (α →ᵇ β) fun _ => α → β := ⟨fun f => f.to_fun⟩ ```

The `coeFun` issue I mentioned is fixed now. Scott's `hom` issue is [still present](https://github.com/leanprover-community/mathlib3port/blob/67a51806c8dd940f81523244e4b9fb47ca980912/Mathbin/CategoryTheory/Category/Basic.lean) though: ```lean class category_struct (obj : Type u) extends Quiver.{v + 1} obj : Type max...

> 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...

I think the Lean 4 default is the right one, I wouldn't change that. > I would guess that in most cases it's not needed since even if there is...

> This worked fine in my own repository - any idea why it wouldn't be working fine here? Unfortunately, we cannot use this for mathlib since `string.to_char_buffer` is excruciatingly slow....

Unfortunately, `put_str` also converts to `char_buffer` under the hood.

I don't think there's anything we can realistically do to fix this in Lean 3. IIRC this will be fixed in Lean 4.

There are six relative imports in total, I think it would be completely okay to just ignore them (for now).

Superseded by #138.