(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals, Errors*" "?0 : Bool → Bool → Bool _21 : ?0 (f false x) y ≡ y [ at Issue2426.agda:17,8-12 ] _22 : ?0 (f false x) y ≡ y [ at Issue2426.agda:17,8-12 ] _23 : ?0 false false ≡ true [ at Issue2426.agda:17,15-19 ] _24 : ?0 false false ≡ true [ at Issue2426.agda:17,15-19 ] ———— Errors ———————————————————————————————————————————————— Issue2426.agda:10,1-9 Incomplete pattern matching for f. Missing cases: f false y when checking the definition of f Failed to solve the following constraints: _23 := refl [blocked on problem 33] [33, 37] ?0 false false = true : Bool _21 := λ {x} {y} → refl [blocked on problem 28] [28, 32] ?0 (f false x) y = y : Bool " nil)
((last . 1) . (agda2-goals-action '(0)))
