Zulip Chat Archive

Stream: new members

Topic: remember


view this post on Zulip petercommand (Nov 01 2018 at 15:13):

Is there something similar to coq's remember tactic in lean?

view this post on Zulip petercommand (Nov 01 2018 at 15:14):

I can't find it in lean's documents

view this post on Zulip Chris Hughes (Nov 01 2018 at 15:14):

What does coq's remember tactic do?

view this post on Zulip petercommand (Nov 01 2018 at 15:15):

It's basically a way to remember a term so that after pattern matching on a non-trivial term, no information is lost

view this post on Zulip Chris Hughes (Nov 01 2018 at 15:17):

Possibly generalize. But I don't fully understand the explanation in the coq docs

view this post on Zulip Reid Barton (Nov 01 2018 at 15:18):

I think cases and/or induction accepts a syntax which lets you name a hypothesis that the thing you pattern matched is equal to the result of the pattern match--is that the sort of thing you mean?

view this post on Zulip petercommand (Nov 01 2018 at 15:19):

yes

view this post on Zulip petercommand (Nov 01 2018 at 15:20):

that's what I want

view this post on Zulip Reid Barton (Nov 01 2018 at 15:20):

Yes, they both have it: the syntax is cases (id :)? expr (with id*)?--check the docstring for full details

view this post on Zulip petercommand (Nov 01 2018 at 15:21):

Thanks!


Last updated: May 16 2021 at 21:11 UTC