idris-1.3.3: test/docs002/expected.out
T1 : Type
Some documentation
The function is: Total & public export
T2 : Type
Some other documentation
The function is: Total & public export
T3 : Int
Some provided postulate
The function is: not yet checked for totality & public export