gebner
commented
2 years ago Woohoo, it actually works (though we've lost the space after the comma somehow)!
def g₂ : Matrix (Finₓ 2) (Finₓ 2) ℤ :=
![![2,-3],![-1,2]]Closed digama0 closed 2 years ago
gebner
commented
2 years ago Woohoo, it actually works (though we've lost the space after the comma somehow)!
def g₂ : Matrix (Finₓ 2) (Finₓ 2) ℤ :=
![![2,-3],![-1,2]]
This is the mathport counterpart of leanprover-community/mathlib4#196, adding support for generating foldl notations. It works to translate the notation itself, but the uses of the notation still do not resolve correctly due to a bug in lean 3 notation name generation that is addressed in leanprover-community/lean#687.