{-# OPTIONS --type-based-termination #-}
data ⊥ : Set where
data T (A : Set) : Set where
sup : (A → T A) → T A
variable A : Set
sup' : (A → T A) → T A
sup' f = f' where f' = sup f
g : T A → ⊥
g (sup f) = g (sup' f)
@ATTN: @knisht
Agda hanging itself here is quite unfair, since I was so close to proving absurdity:
Type-based termination succeded for definitions
[g]
e : T ⊥
e = sup λ()
false : ⊥
false = g e
It seems that Agda hangs in the injectivity checker when trying to reduce g.
Agda seems to loop on this example:
@ATTN: @knisht
Agda hanging itself here is quite unfair, since I was so close to proving absurdity:
It seems that Agda hangs in the injectivity checker when trying to reduce
g
.