simp lemma?

Stream: general

[Kenny Lau]

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

[Kenny Lau]

Should this be a simp lemma?

[Kenny Lau]

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

[Chris Hughes]

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

[Mario Carneiro]

this won't trigger because the LHS is arbitrary

[Johan Commelin]

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]

this won't trigger because the LHS is arbitrary

why does that mean it wouldn't trigger?

[Kenny Lau]

is it because it's a loop?

[Simon Hudon]

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