Agda2> (agda2-status-action "") (agda2-info-action "*Type-checking*" "" nil) (agda2-highlight-clear) (agda2-info-action "*Type-checking*" "Checking Issue1083 (Issue1083.agda).\n" t) (agda2-info-action "*Type-checking*" "Finished Issue1083.\n" t) (agda2-status-action "") (agda2-info-action "*All Goals*" "?1 : T false\n_x_9 : Bool [ at Issue1083.agda:16,13-14 ]\n_11 : Bool → Bool [ at Issue1083.agda:16,13-19 ]\n" nil) ((last . 1) . (agda2-goals-action '(0 1))) Agda2> (agda2-give-action 1 "true") (agda2-status-action "") (agda2-info-action "*All Goals*" "_x_9 : Bool [ at Issue1083.agda:16,13-14 ]\n_11 : Bool → Bool [ at Issue1083.agda:16,13-19 ]\n" nil) ((last . 1) . (agda2-goals-action '(0))) Agda2> (agda2-info-action "*Error*" "\nNo type nor action available for hole ?0" nil) (agda2-highlight-load-and-delete-action) (agda2-status-action "") Agda2>