Quasiquote004.idr:39:26-31: This style of tactic proof is deprecated. See %runElab for the replacement. Quasiquote004.idr:42:28-33: This style of tactic proof is deprecated. See %runElab for the replacement. Quasiquote004.idr:50:27-32: This style of tactic proof is deprecated. See %runElab for the replacement. Quasiquote004.idr:50:25: When checking right hand side of Quasiquote004.getMeNat' with expected type String Not a Nat goal