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