[Agda] rewrite vs. with

[Jean-Philippe Bernardy]

You should first abstract on the term (use 'with' on it) and then use
with on the witness of equality.
These two operations are conveniently packaged for you in the form of
the 'rewrite' lhs:

g A t B f b1 b2 rewrite eq t = ?

Cheers,
JP.

On Tue, Sep 28, 2010 at 7:07 AM, David Leduc
<david.leduc6 at googlemail.com> wrote:
> Hi,
>
> Sorry, it's again a newbie question.
> In the code below, I'd like to replace the hole in g with f b1 b2.
> The problem is that f takes two arguments of the same type,
> but the type of b1 and b2 are only provably equal (with Lemma eq).
> In Coq I would use the tactic rewrite.
> In Agda, I guess I should use a "with" but it does not work in this case.
> I get the following error message:
>
>  Cannot pattern match on constructor refl, since the inferred
>  indices [proj1 t'] cannot be unified with the expected indices
>  [proj2 t'] for some t', A'
>  when checking that the expression ? has type A
>
> What can I do?
>
> --------------------------------
>
> module test where
>
> open import Relation.Binary.PropositionalEquality
>
> data T (A : Set) : Set where
>  makeT : (a1 a2 : A) -> a1 ≡ a2 -> T A
>
> proj1 : {A : Set} -> T A -> A
> proj1 (makeT a _ _) = a
>
> proj2 : {A : Set} -> T A -> A
> proj2 (makeT _ a _) = a
>
> eq : {A : Set}(t : T A) -> proj1 t ≡ proj2 t
> eq (makeT _ _ p) = p
>
> g : (A : Set)(t : T A)(B : A -> Set)(f : B (proj1 t) -> B (proj1 t) -> A)
>  (b1 : B (proj1 t))(b2 : B (proj2 t)) -> A
> g A t B f b1 b2 with eq t
> ...| p = {!!}
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>