(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals, Errors*" "?0 : _B_42 (f = f) (r = r) x _B_42 : Nat → Set [ at Issue4982.agda:25,41-42 ] ———— Errors ———————————————————————————————————————————————— Failed to solve the following constraints: f x =< ?0 (f = f) (r = r) (x = 0) x : A (blocked on _48) ?0 (x = 0) = f : _B_42 0 (blocked on _48) _B_42 0 = A → A : Set (blocked on _B_42) " nil)
((last . 1) . (agda2-goals-action '(0)))
(agda2-status-action "")
(agda2-info-action "*Goal type etc.*" "Goal: _B_42 (f = f) (r = r) x ———————————————————————————————————————————————————————————— x : Nat (not in scope) r : R f f : A → A ———— Constraints ——————————————————————————————————————————— f x₁ =< ?0 (f = f) (r = r) (x = 0) x₁ : A (blocked on _48, belongs to problem 67) ?0 (x = 0) = f : _B_42 (f = f) (r = r) 0 (blocked on _48, belongs to problem 58) _51 := λ f r → r (blocked on problem 67) _49 := λ f r → cong ((x : Nat) → _B_42 (f = f) (r = r) x) (_B_42 (f = f) (r = r) 0) (λ z → ?0 (f = f) (r = r) (x = z)) (λ z → ?0 (f = f) (r = r) (x = z)) (λ f₁ → apply Nat (λ v → _B_42 (f = f) (r = r) v) f₁ 0) (refl ((x : Nat) → _B_42 (f = f) (r = r) x) (λ z → ?0 (f = f) (r = r) (x = z))) (blocked on problem 58) _43 := λ f r → _B_42 (f = f) (r = r) 0 (blocked on problem 59, belongs to problem 58)" nil)
