Base.IdrTest [0.0.1]

Unit-test framework for Idris2


IdrTest is a unit-test library for Idris2. Idris allows developers to write dependently-typed and provably correct code, but sometimes there's no substitute for a simple unit test.

For instance, consider: reverse : List a -> List a. A unit test can easily add some confidence this function runs correctly (at least in some cases). It would be better to write a function that codes the meaning of reverse in its types, but in lieu of that, a unit test is helpful.

Getting Started

Add Base.IdrTest=^0.0.1 to Inigo.toml and run inigo prod fetch-deps. You should add a directory Test and copy in the following skeleton to Test/Suite.idr:

module Test.Suite

import IdrTest.Test

myTestSuite : Test
myTestSuite =
	describe "My Tests" [
		test "Simple Math" (\_ => assertEq (2+2) 4)

suite : IO ()
suite = do
    [ myTestSuite

To run your tests, run:

inigo test

or you can run them directly via:

idris2 --find-ipkg Test/Suite.idr -x suite


Currently there are three expecatations:

assertEq : Show a => Eq a => a -> a -> Expectation

assertEq will test that two things are the same and return an error if they are not.

fail : String -> Expectation

pass : Expectation

pass and fail will always pass or fail a test respectively. You can use these functions to build more complex behaviors in your tests.


These tests are not meant to replace building correctness into your dependently-typed program. They are simply meant as a helpful addition to your Idris tool-chain. Additionally, IO and foreign-function calls may be difficult to test with IdrTest.


Feel free to grow and expand IdrTest to add new expectations or better handling of tests or failures.


This code is licensed under the MIT license. All contributors must release all code under this same license.


* 0.0.1