tensors / array programming

Stream: Is there code for X?

[Jianlin Li]

Hi everyone :blush:
I was wondering if anyone knows of an existing Lean mechanization for NumPy-style arrays, tensors, or NamedTensors?
I’m curious about both pointful and point-free styles of array programming! :folded_hands: