The full working code for the TyDe 2024 paper submitted by Thomas Ekström Hansen and Edwin Brady .

A working install of the Idris2 compiler >= v0.7.0 is required. The easiest way to get this set up is to install Idris2 via pack.

With a working idris2 in your $PATH, the files can be compiled by running

idris2 --build tyde24.ipkg

An interactive REPL session can be started by running

idris2 --repl tyde24.ipkg

This will load the Generic module by default. The other modules can be loaded by running the REPL command

:module ModuleName

(replacing ModuleName with the name of the module to additionally load.)

After a module has been loaded, its contents can be browsed via the REPL command

:browse ModuleName

The code in this repository is licensed under the terms of the BSD-3-Clause license (see the LICENSE file).