Zulip Chat Archive

Stream: new members

Topic: remember

petercommand (Nov 01 2018 at 15:13):

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

petercommand (Nov 01 2018 at 15:14):

I can't find it in lean's documents

Chris Hughes (Nov 01 2018 at 15:14):

What does coq's remember tactic do?

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

Chris Hughes (Nov 01 2018 at 15:17):

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

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?

petercommand (Nov 01 2018 at 15:19):

yes

petercommand (Nov 01 2018 at 15:20):

that's what I want

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

petercommand (Nov 01 2018 at 15:21):

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC