[Agda] Termination problem with --without-K

[Andreas Abel]

This issue is fixed now on master (and maint-2.4.0).  The fix will be 
included in the upcoming release.

On 28.08.14 11:40 AM, Andreas Abel wrote:
> 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/