[Agda] binding variables in rewrite pragma
Michael Shulman
shulman at sandiego.edu
Sat Sep 21 00:22:55 CEST 2019
I've been playing around with the REWRITE pragma, and I'm getting an
error message that I don't understand:
{-# OPTIONS --rewriting #-}
infix 10 _⟼_
postulate
_⟼_ : {A : Set} → A → A → Set
{-# BUILTIN REWRITE _⟼_ #-}
data _×_ (A B : Set) : Set where
_,_ : A → B → A × B
fst : (A B : Set) (s : A × B) → A
fst A B (x , y) = x
postulate
foo : {A : Set} (B : A → Set) → Set
foo0 : {A : Set} (B C : A → Set) → foo B
bar : {A : Set} (B : A → Set) (f : (x : A) → B x) → foo B
bar-fst : (A : Set) (B C : A → Set) (u : (x : A) → B x × C x)
→ bar B (λ (x : A) → fst (B x) (C x) (u x)) ⟼ foo0 B C
{-# REWRITE bar-fst #-}
This produces the error
"bar-fst is not a legal rewrite rule, since the following variables
are not bound by the left hand side: C
when checking the pragma REWRITE bar-fst"
I don't understand why C is not bound by the LHS. Can anyone explain?
More information about the Agda
mailing list