Some coercions are not expanded during binport

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4

Apache License 2.0

43 stars 15 forks source link

Some coercions are not expanded during binport #117

Closed gebner closed 2 years ago

gebner commented 2 years ago

#check ContinuousLinearMap.to_linear_map_eq_coe
/-
ContinuousLinearMap.to_linear_map_eq_coe : ∀ (f : ?m.8001 →SL[?m.8000] ?m.8004), f.toLinearMap = coe f
-/

Presumably related to the contained coeBaseₓ instance which has a CoeTₓ type.

gebner commented 2 years ago

Related to #17. That issue was about the Lean elaborator not expanding coercions, which should work fine now. This issue is about the binporter not expanding coercions.