1
module ConstructorHeadedDivergenceIn2-2-10 where
10
data _×_ (A B : Set) : Set where
13
{- Brandon Moore reports (July 2011)
14
In 2.2.10 the following code seems to cause typechecking
24
enum (suc n) = n , enum n
32
This typechecks quickly if the definition
37
I think the problem is that the body has type ℕ × f n,
38
and unifying it with the expected type f n invokes the
39
constructor-headed function specialization to resolve
40
n to suc n', and the process repeats.
b'\\ No newline at end of file'