Skip to content

Dependently typed N-dimensional array type signatures for Idris (2).

Notifications You must be signed in to change notification settings

bobbbay/dinwiddy

Repository files navigation

Dinwiddy

N-dimensional arrays in Idris 2, featuring:

  • Nat-indexable n-dimensional array type synonyms
  • Matrices and matrix algebra helper functions

Usage

At a very basic level, the API for an N-dimensional array in Dinwiddy is the following:

Array : (dimension : Nat) -> (sizes : Vect dimension Nat) -> (type : Type)

For example, the following type declaration x:

x : Array 2 [2, 3] Bool

Will create an array that looks like this:

###
###

Full of booleans. It’s value could be, for example:

x = [[ True,  True,  True ],
     [ False, False, True ]]

Check out `examples` and `tests` for more information.

About

Dependently typed N-dimensional array type signatures for Idris (2).

Topics

Resources

Stars

Watchers

Forks