# [Agda] "metavariable" message

Sergei Meshveliani mechvel at botik.ru
Sun Nov 3 19:22:45 CET 2013

```People,
I have the two questions about the below program.

1) Why the checker reports about "metavariable" ?

(Agda 2.3.2.2 MAlonzo).

2) How to prove  toDgs'-suc=toDgs-suc ?

The statement looks as trivial,
and  " → blRefl"  needs to be sufficient in the last branch.
But it fails.

Thank you in advance for explanation,

------
Sergei

--------------------------------------------------------------
open import Function using (_\$_; _∘_; case_of_)
open import Relation.Binary using
(IsEquivalence; module IsEquivalence; Setoid;
module Setoid; DecSetoid; module DecSetoid;
DecTotalOrder; module DecTotalOrder
)
open import Relation.Binary.PropositionalEquality as PE
using (_≡_)
open import Data.Empty      using (⊥; ⊥-elim)
open import Data.Unit       using (⊤)
open import Data.Fin as Fin using (Fin)
renaming (zero to 0b; suc to sucF)
import Data.Fin.Props as FinP using (decSetoid)
open import Data.Digit using (Bit)
open import Data.Bin   using (Bin⁺)
open import Data.Digit using (toDigits; fromDigits)
open import Data.Product    using (_×_; _,_; proj₁; proj₂; ∃)
open import Data.Nat as Nat using (ℕ; suc)
renaming (decTotalOrder to natDTO)
open import Data.List     using (List; []; _∷_)
open import Relation.Binary.List.Pointwise as LP using ()

-------------------------------------------------------------------
bitDecSetoid = FinP.decSetoid 2
open DecSetoid bitDecSetoid using () renaming (setoid to bitSetoid)
blSetoid = LP.setoid bitSetoid
open Setoid blSetoid using ()
renaming (_≈_ to _=l_; isEquivalence to blEquiv)
open IsEquivalence blEquiv using ()
renaming (refl to blRefl; sym to blSym)

postulate anything : ∀ {a} {A : Set a} → A  -- for debug

toDgs = proj₁ ∘ toDigits 2

toDigits' : (n : ℕ) → ∃ \ (bs : Bin⁺) → fromDigits bs ≡ n
toDigits' n  with  toDigits 2 n

... | ([]      , eq) =  ([]     , eq)  -- inaccessible
... | (0b ∷ [] , eq) =  ([]     , eq)
... | (b ∷ bs  , eq) =  (b ∷ bs , eq)
--
-- It differs from  toDigits  only at  n = 0.

toDgs' = proj₁ ∘ toDigits'

toDgs'-suc=toDgs-suc : ∀ n → toDgs' (suc n) =l toDgs (suc n)
toDgs'-suc=toDgs-suc 0       = blRefl
toDgs'-suc=toDgs-suc (suc n) =
case
toDigits 2 (suc (suc n))
of \
{ ([]                    , ())
; (0b ∷ []               , ())
; ((sucF 0b) ∷ []        , ())
; ((sucF (sucF ())) ∷ [] , _ )
; (b ∷ b' ∷ bs           , _ ) →
let gl : toDgs' (suc \$ suc n) =l (b ∷ b' ∷ bs)
-- toDgs (suc \$ suc n)
gl = anything
in  gl
}

```