idris-1.3.3: test/interactive012/input.in
:t mkString_rhs_1 :t mkString_rhs_2 :t mkThing_rhs_1 :t mkThing_rhs_2 :t mkString2_rhs :t mkString3_rhs_1 :t mkString3_rhs_2 :t append_rhs_1 :t append_rhs_2
:t mkString_rhs_1 :t mkString_rhs_2 :t mkThing_rhs_1 :t mkThing_rhs_2 :t mkString2_rhs :t mkString3_rhs_1 :t mkString3_rhs_2 :t append_rhs_1 :t append_rhs_2