Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]

[Andreas Abel]

Mmh, the easiest fix is: trash the builtin NATDIVSUCAUX.  I do not know 
what it is for.  The only use I found for it was in

   example/lib/Data/Nat.agda

with the definition you have given below.

The standard library does not seem to use it.

I propose removal, alongside with NATMODSUCAUX.  If you oppose this, 
speak up now!

Cheers,
Andreas

On 23.04.12 4:24 AM, James Deikun wrote:
> I know this one isn't currently used in the standard library, but I was
> poking around the defined builtins and primitives in my FastNat work and
> I discovered this short proof of false:
>
> module Test where
>    open import Data.Nat
>    open import Data.Empty
>    open import Relation.Binary.PropositionalEquality
>
>    0≢1+n : ∀ {n} ->  0 ≢ suc n
>    0≢1+n ()
>
>    divSucAux : (k m n j : ℕ) ->  ℕ
>    divSucAux k m zero j = k
>    divSucAux k m (suc n) zero = divSucAux (suc k) m n m
>    divSucAux k m (suc n) (suc j) = divSucAux k m n j
>    {-# BUILTIN NATDIVSUCAUX divSucAux #-}
>
>    oh-noes : ⊥
>    oh-noes = 0≢1+n {divSucAux 0 0 0 1} refl
>
> Probably an easy fix, just a retool of the fast path for NATDIVSUCAUX to
> never return anything less than k.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
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/