poor man's hint database

Stream: general

[Moses Schönfinkel]

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]

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

[Mario Carneiro]

you can write simp with x_lemmas

[Moses Schönfinkel]

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]

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

[Mario Carneiro]

It would be unusual, but not unheard of

[Moses Schönfinkel]

good enough, thanks

[Mario Carneiro]

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

[Kenny Lau]

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]

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

[Mario Carneiro]

?

[Mario Carneiro]

what does that have to do with my quote

[Kenny Lau]

well that means the default simp set is much bigger

[Mario Carneiro]

I said it is not a superset