Zulip Chat Archive

Stream: new members

Topic: Coq equivalent to eapply/erewrite

Vincent Siles (Sep 28 2020 at 14:51):

Hi ! I'm slowly getting to know Lean, from a Coq background, and I'm wondering if there's equivalent to Coq's Evar (introduced by eapply/erewrite/refine/ ...) ?

Johan Commelin (Sep 28 2020 at 15:47):

We have erw and refine. But I don't know Evar, so I don't know if it's what you are looking for (@Vincent Siles)

Pedro Minicz (Sep 28 2020 at 18:24):

It has been a while since I've used Coq, but, as far as I remember, erewrite/eapply etc add the existential goals when it can't resolve arguments. As far as my experience goes, Lean's default rw/apply mostly behaves like the existential variants in Coq.

Last updated: Dec 20 2023 at 11:08 UTC