[Agda] Termination problem with --without-K

[Andreas Abel]

Thanks for reporting!  I am in the process of fixing it.  --Andreas

On 28.08.14 3:02 AM, Jacques Carette wrote:
>
> {-# OPTIONS --without-K #-}
>
> open import Data.List
> open import Data.Nat
> open import Data.Bool
>
> module Sort (A : Set) ( _≤_ : A → A → Bool) where
> insert : A → List A → List A
> insert x [] = []
> insert x (y ∷ ys) with x ≤ y
> ... | true = x ∷ y ∷ ys
> ... | false = y ∷ insert x ys

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/