search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
40 stars 15 forks source link

feat: add support for `matrix.notation` #235

Closed digama0 closed 1 year ago

digama0 commented 1 year ago
eric-wieser commented 1 year ago

CI is failing and there are conflicts. I assume the lake manifest update is no longer relevant and master already contains the change you need.

eric-wieser commented 1 year ago

Can you run this against mathlib's test/matrix.lean just to check it behaves in the corner cases? Otherwise I guess we just merge it and see what happens on some of mathlibs's src files

semorrison commented 1 year ago

This is blocking progress on the longest chain in the port, so I'm just going to merge now and hope for the best. :-)