Comment by m_j_g

It is nice to see practical application of dependently typed language!