Dependently Typed Einstein Summation

May 19, 2019 ยท View on GitHub

Implementing a dependently typed Einstein summation in Idris, inspired by Python's numpy.

The main idea is to provide a typed version of einsum.

Work in progress