The full working code for the
TyDe 2024
paper submitted by
Thomas Ekström Hansen 
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).