{-# OPTIONS --no-syntax-based-termination #-}
{-# OPTIONS --type-based-termination #-}
module TypeBasedTermination.CopatternNonterminating where
open import Agda.Builtin.Equality
record Stream (A : Set) : Set where
coinductive
field
head : A
tail : Stream A
module S = Stream
illdefined : {A : Set} → Stream A
S.head illdefined = S.head illdefined
S.tail illdefined = S.tail illdefined
-- should not termination-check
The error is:
15,1-17,38
Termination checking failed for the following functions:
Problematic calls:
The error is:
The error should be about function
illdefined
.This issue has been reported before in