idris-0.10.1: test/idrisdoc004/TestTypeclasses.idr
module TestTypeclasses ||| This is a test ||| ||| @ a Test arg public export interface Test a where ||| Test function test : a -> Int
module TestTypeclasses ||| This is a test ||| ||| @ a Test arg public export interface Test a where ||| Test function test : a -> Int