Zulip Chat Archive

Stream: general

Topic: simp lemma?


Kenny Lau (Mar 16 2019 at 23:06):

@[simp] lemma eq_default {α : Sort*} [inhabited α] [subsingleton α] (x : α) : x = default α :=
subsingleton.elim _ _

Kenny Lau (Mar 16 2019 at 23:06):

Should this be a simp lemma?

Kenny Lau (Mar 16 2019 at 23:06):

Or maybe should we say that all punits are punit.star instead?

Chris Hughes (Mar 17 2019 at 03:09):

I seem to remember trying a simp lemaa like this ages ago and it never triggering.

Mario Carneiro (Mar 17 2019 at 03:10):

this won't trigger because the LHS is arbitrary

Johan Commelin (Mar 17 2019 at 05:56):

If you are inhabited and subsingleton than you are unique. I wrote a tiny api for unique some time ago. Does that help, or is it maybe not constructive enough for your purposes?

Kenny Lau (Mar 17 2019 at 09:27):

this won't trigger because the LHS is arbitrary

why does that mean it wouldn't trigger?

Kenny Lau (Mar 17 2019 at 09:27):

is it because it's a loop?

Simon Hudon (Mar 18 2019 at 02:09):

It doesn’t trigger because its RHS is only a variable, therefore no head symbol to match on


Last updated: Dec 20 2023 at 11:08 UTC