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