Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?

Agda rewrite bug (Update at end)

Agda version: 2.5.1.1 OSX: 10.11.5

This definitely seems to be a bug this time, when trying to use the rewrite functionality on implementing Conor and James' Levitation With A Lambda paper I have the following code (fragment):

actNVaIm {Γ} (Λ' b T) t rewrite wkAcVaIm {Γ} b = ?

Trying to load the file, the following error is displayed:

No binding for builtin thing EQUALITY, use {-# BUILTIN EQUALITY
name #-} to bind it to 'name'
when checking that the clause
actNVaIm {Γ} (Λ' b T) t rewrite wkAcVaIm {Γ} b = ? has type
{Γ : Bwd B} (D : Desc) (tn : Node Tm Γ D) → actN vaIm D tn ≃ tn

In fact, the actNVaIm function in the paper uses rewrite many times, and they all fail with the same "binding" error

Update

I've gotten round the problem by introducing a new lemma and using that lemma to write the term as

actNVaIm {Γ} (Λ' b T) t = actVaAB (actNVaIm T t) (wkAcVaIm {Γ} b)

where

actVaAB : ∀ {Γ} {D} {t : Node Tm Γ D} {a} {b}
          → actN a D t ≃ t
          → a ≃ b
          → actN b D t ≃ t
actVaAB p refl = p

Taking advantage of the pattern a in the actN term equality.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment