## Stream: general

### Topic: poor man's hint database

#### Moses Schönfinkel (Nov 19 2018 at 08:21):

Is there a way to simulate Coq's hint database? For example, I often find myself writing simp [x₁, x₂, x₃, x₄], which I would like to replace with simp [x_lemmas] where x_lemmas is a sort of a "hint database" for lack of better term. (Do note that I don't want to designate xₙ to be simp lemmas.)

#### Mario Carneiro (Nov 19 2018 at 08:24):

there are simp sets, but we don't use them very often

#### Mario Carneiro (Nov 19 2018 at 08:24):

you can write simp with x_lemmas

#### Moses Schönfinkel (Nov 19 2018 at 08:25):

Where x_lemmas is a "simp set"? Would it be weird for you to encounter that somewhere in Lean code - is that something to avoid?

#### Mario Carneiro (Nov 19 2018 at 08:26):

The "default" simp set is not necessarily a superset of other simp sets, so it should be fine

#### Mario Carneiro (Nov 19 2018 at 08:26):

It would be unusual, but not unheard of

#### Moses Schönfinkel (Nov 19 2018 at 08:26):

good enough, thanks

#### Mario Carneiro (Nov 19 2018 at 08:26):

It forms part of the public interface, so I don't use it for one off things

#### Kenny Lau (Nov 19 2018 at 09:12):

The "default" simp set is not necessarily a superset of other simp sets, so it should be fine

No. We have demonstrated more than once that using a simp set speeds things up.

#### Kenny Lau (Nov 19 2018 at 09:12):

I don’t know why you don’t like it.

?

#### Mario Carneiro (Nov 19 2018 at 09:18):

what does that have to do with my quote

#### Kenny Lau (Nov 19 2018 at 09:20):

well that means the default simp set is much bigger

#### Mario Carneiro (Nov 19 2018 at 09:22):

I said it is not a superset

Last updated: May 10 2021 at 23:11 UTC