Re: [isabelle] Opposite of the `transfer` method
> I’m wondering how others reason with equivalence relations. Somehow I
> can’t imagine that a situation like mine is so rare; so I’d be
> if there isn’t an approach to performing “equivalence reasoning”
> conveniently. Any hints?
Coq has a setoid rewrite engine, which might be what you want here?.
The idea is to rewrite wrt arbitrary preorders.
Up to my knowledge, such a thing has not yet been implemented in
Isabelle (though I'm collecting possible applications, as I might
implement such a thing sooner or later ;) )
> All the best,
This archive was generated by a fusion of
Pipermail (Mailman edition) and