Agda.Termination.SparseMatrix

Basic data types

data Matrix i b

matrixInvariant

data Size i

sizeInvariant

data MIx i

mIxInvariant

Generating and creating matrices

fromLists

fromIndexList

toLists

matrix

matrixUsingRowGen

Combining and querying matrices

size

square

isEmpty

isSingleton

add

intersectWith

mul

transpose

diagonal

Modifying matrices

addRow

addColumn

Tests

tests