Evaluate term to normal form yields a stack overflow

[UlfNorell]

From andres.s...@gmail.com on August 01, 2013 06:53:26

module Bug where

infixr 8 ^ infixl 7 * infixl 6 +

data ℕ : Set where zero : ℕ succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-} {-# BUILTIN ZERO zero #-} {-# BUILTIN SUC succ #-}

+ : ℕ → ℕ → ℕ zero + n = n succ m + n = succ (m + n)

* : ℕ → ℕ → ℕ zero * n = zero succ m * n = n + m * n

^ : ℕ → ℕ → ℕ m ^ zero = 1 m ^ succ n = m * m ^ n

-- C-c C-n (Evaluate term to normal form): 2 ^ 16

-- Result: 65536

-- C-c C-n (Evaluate term to normal form): 2 ^ 17 -- Result: stack overflow

Original issue: http://code.google.com/p/agda/issues/detail?id=885

[UlfNorell]

From andres.s...@gmail.com on August 01, 2013 05:04:16

Summary: Evaluate term to normal form yields a stack overflow (was: Stack overflow)

[UlfNorell]

From andres.s...@gmail.com on August 01, 2013 08:53:56

Status: Invalid
Labels: -Type-Defect