[Agda] suc suc _ : Bit

[Andreas Abel]

The fix is to also supply the non-hidden argument.  An underscore 
suffices.

   positive-add1 {sucB (sucB ()) ∷ _} _

But agreed, the error message you get is horrible.  I filed this as 
issue 919.

On 2013-10-12 03:17, Sergei Meshveliani wrote:
> Please, how to fix the below  positive-add1  (last clause) ?
>
> --------------------------------------------------------------------
> open import Level using () renaming (zero to 0ℓ)
> open import Relation.Nullary.Core using (¬_)
> open import Data.Empty using (⊥; ⊥-elim)
> open import Data.List  using ([]; _∷_)
> open import Data.Fin   using (Fin) renaming (zero to 0b; suc to sucB)
> open import Data.Digit using (Bit)
> open import Data.Bin   using (Bin⁺; addCarryToBitList)
>
> 1b : Bit
> 1b = sucB 0b
>
> add1 : Bin⁺ → Bin⁺
> add1 = addCarryToBitList 1b
>
> data Positive : Bin⁺ → Set      -- "ends with 1"
>   where
>   single : Positive (1b ∷ [])
>   cons   : {b : Bit} → {bs : Bin⁺} → Positive bs → Positive (b ∷ bs)
>
> test : Bit → Bit            -- testing  (sucB (sucB ()))
> test 0b               = 0b
> test (sucB 0b)        = 0b
> test (sucB (sucB ()))
>
> positive-add1 : {bs : Bin⁺} → Positive bs → Positive (add1 bs)
>
> positive-add1 {0b ∷ _}       (cons pos-bs) =  cons pos-bs
> positive-add1 {sucB 0b ∷ []} single        =  cons single
> positive-add1 {sucB 0b ∷ _}  (cons pos-bs) =
>                                            cons (positive-add1 
> pos-bs)
> positive-add1 {sucB (sucB ()) ∷ _}
> --------------------------------------------------------------------
>
> 1. Agda always insists on the presence of the pattern  sucB (sucB _),
> as if it does not see that it is not in  Bit = Fin 2.
>
> 2. All right, I use the pattern  (sucB (sucB ()))  to eliminate the
> case.
> This does work in `test', and also in the version of  positive-add1' 
> --
> which has  bs  as explicit.
> But it is not type-checked in the `implicit' version.
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
>
> _______________________________________________
> 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 
http://www.tcs.informatik.uni-muenchen.de/~abel/