data TestOutcome : Type Outcome of a single test for structured reporting.
Totality: total
Visibility: public export
Constructors:
Passed : Integer -> TestOutcome Failed : FailureInfo -> Integer -> TestOutcome Skipped : Maybe String -> TestOutcome
record TestReport : Type A completed test with its describe path, source location, and outcome.
Totality: total
Visibility: public export
Constructor: MkTestReport : List String -> Maybe SrcLoc -> TestOutcome -> TestReport
Projections:
.loc : TestReport -> Maybe SrcLoc .outcome : TestReport -> TestOutcome .path : TestReport -> List String
.path : TestReport -> List String- Visibility: public export
path : TestReport -> List String- Visibility: public export
.loc : TestReport -> Maybe SrcLoc- Visibility: public export
loc : TestReport -> Maybe SrcLoc- Visibility: public export
.outcome : TestReport -> TestOutcome- Visibility: public export
outcome : TestReport -> TestOutcome- Visibility: public export
nanosToSeconds : Integer -> String Convert nanoseconds to "S.MMMMs" (no unit suffix). Shared by reporters.
Visibility: export