Zulip Chat Archive

Stream: general

Topic: simp lemma?


view this post on Zulip Kenny Lau (Mar 16 2019 at 23:06):

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

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:06):

Should this be a simp lemma?

view this post on Zulip Kenny Lau (Mar 16 2019 at 23:06):

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

view this post on Zulip Chris Hughes (Mar 17 2019 at 03:09):

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

view this post on Zulip Mario Carneiro (Mar 17 2019 at 03:10):

this won't trigger because the LHS is arbitrary

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Mar 17 2019 at 09:27):

is it because it's a loop?

view this post on Zulip 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: May 08 2021 at 20:11 UTC