## Stream: general

### Topic: unknown local constant: _ffresh.0

#### Scott Morrison (Jun 30 2019 at 22:37):

Has anyone seen an otherwise successful def error with unknown local constant: _ffresh.0?

#### Simon Hudon (Jun 30 2019 at 22:41):

do you use variable or parameter? Do you use include?

#### Scott Morrison (Jun 30 2019 at 22:43):

Yes to all of the above. :-) Changing the name of an argument of the function solved the problem.... Looks bug-ish to me, but I don't have time to minimise now so will proceed with slightly strange argument names!

#### Simon Hudon (Jun 30 2019 at 22:44):

you probably have variable x, assumption h mentioning x, include h and then you declare x as an argument to your definition

#### Simon Hudon (Jun 30 2019 at 22:45):

Lean does not include the variable but includes h

Last updated: May 13 2021 at 19:20 UTC