[Agda] binding variables in rewrite pragma
Andreas Abel
andreas.abel at ifi.lmu.de
Sat Sep 21 12:41:48 CEST 2019
It is a bug: https://github.com/agda/agda/issues/4103
The issue description contains suggestions for a workaround.
On 2019-09-21 10:14, Andreas Abel wrote:
> 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
>>
More information about the Agda
mailing list