## 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?

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: May 16 2021 at 21:11 UTC