(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals, Errors*" "?0 : Set → Set ?1 : ?0 T ?2 : Set ?3 : Id ?2 (?1 tt) ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: T → ?2 = ?0 T : Set (blocked on _P_12) " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3)))
(agda2-give-action 3 "h")
(agda2-status-action "")
(agda2-info-action "*All Goals, Errors*" "?0 : Set → Set ?1 : ?0 T ?2 : Set ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: tt = ?1 tt : T (blocked on any(_P_12, _u_13)) T → T = ?0 T : Set (blocked on _P_12) " nil)
((last . 1) . (agda2-goals-action '(0 1 2)))
