Tester

Reexports

Definitions

TestFunc : Type -> Type

  A function which can report test failures.

Visibility: public export

record Test : Type

  Value representing a test.
  
  Use the `test` function to create a value of this type.

Totality: total
Visibility: public export
Constructor: 

MkTest : String -> TestFunc () -> Test

Projections:

.description : Test -> String

.run : Test -> TestFunc ()

.description : Test -> String

Visibility: public export

description : Test -> String

Visibility: public export

.run : Test -> TestFunc ()

Visibility: public export

run : Test -> TestFunc ()

Visibility: public export

test : String -> TestFunc () -> Test

  Create a new `Test` with a description and function to run.
  
  Use `Test.Runner.runTests` to run the tests.
  
  ```idris example
  itWorks = test "it works" $ do
      assertEq (1 + 1) 2
  ```

Visibility: public export

record Location : Type

Totality: total
Visibility: public export
Constructor: 

Loc : FC -> Location

Projection: 

.inner : Location -> FC

.inner : Location -> FC

Visibility: public export

inner : Location -> FC

Visibility: public export

emptyLoc : Location

Visibility: export

here : TTImp -> Elab Location

  Get a `Location` token
  This can be passed to assertion to attach source location
  
  ```idris example
  let loc = here `(())
   in assertEq {loc} 

Visibility: export

formatLoc : Location -> String

Visibility: export

assertEq : (Eq a, Show a) => {default emptyLoc _ : Location} -> a -> a -> TestFunc ()

  Assert that two values are equal.
  
  Stops the test and reports a test failure if the values are not equal.

Visibility: public export

assertNotEq : (Eq a, Show a) => {default emptyLoc _ : Location} -> a -> a -> TestFunc ()

  Assert that two values are not equal.
  
  Stops the test and reports a test failure if the values are equal.

Visibility: public export

assert : {default emptyLoc _ : Location} -> Bool -> TestFunc ()

  Assert that a condition holds.
  
  Stops the test and reports a test failure if the condition does not hold.

Visibility: public export

throw : String -> TestFunc a

  Cause a test failure with a message.

Visibility: public export