def MatT.eye
import bend-tensors@0.0.0.2/bend_tensors.bend as BendTensorsimport Base
716# the identity of MatT(n, n)
717def MatT.eye(+n: Nat) -> MatT(n, n):
718 match n:
719 case 0n:
720 MatB{Blk.eye()}
721 case 1n+p:
722 a b c d = MatT.eye(p) MatT.zeros(p, p) MatT.zeros(p, p) MatT.eye(p)
723 MatQ{a, b, c, d}