idris-0.9.20.1: test/interactive012/input
: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