## Stream: general

### Topic: dsimp doesn't work with abbreviations

#### Scott Morrison (Jul 11 2020 at 09:06):

def f := 1
abbreviation g := f

example : f = g :=
begin
-- dsimp [g], -- fails
dunfold g, -- we have to know to use dunfold for abbreviations :-(
refl,
end


Is this potentially fixable? It's currently an annoying thing to have to remember about abbreviation.

#### Kenny Lau (Jul 11 2020 at 09:07):

use notation

Last updated: May 14 2021 at 07:19 UTC