search

lecopivo / SciLean

Scientific computing in Lean 4
https://lecopivo.github.io/scientific-computing-lean/
Apache License 2.0
328 stars 29 forks source link

odd interaction with `Id` #47

Open alok opened 1 day ago

alok commented 1 day ago

import SciLean breaks some of my code, even if I don't use it directly. Unsure why, but here's a diagnostic, where Coe Id' seem to be synthesized a lot

2024-11-21-02-10-16

alok commented 1 day ago

If I change the * on line 42 to .matmul it works fine though. So something is messing with my hmul instance in scilean

2024-11-21-02-12-21

lecopivo commented 12 hours ago

Can you give me mwe?

lecopivo commented 12 hours ago

I fixed one instance with Id', does that fix your problem?

alok commented 12 hours ago

I'll try it out and report

On Fri, Nov 22 2024 at 11:05, Tomáš Skřivan < @.*** > wrote:

I fixed one instance with Id' ( https://github.com/lecopivo/SciLean/commit/d43e4f3df99e2a7772355d4163911f3d977f7d42 ) , does that fix your problem?

— Reply to this email directly, view it on GitHub ( https://github.com/lecopivo/SciLean/issues/47#issuecomment-2494591306 ) , or unsubscribe ( https://github.com/notifications/unsubscribe-auth/AB7QUTD52MZMF64CM7T6CAD2B557RAVCNFSM6AAAAABSGTQNW2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIOJUGU4TCMZQGY ). You are receiving this because you authored the thread. Message ID: <lecopivo/SciLean/issues/47/2494591306 @ github. com>