[Agda] binding variables in rewrite pragma

[Andreas Abel]

This could be a bug, I started to investigate; I'll get back to you on 
this.  --Andreas

On 2019-09-21 00:22, Michael Shulman wrote:
> 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?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>