Zulip Chat Archive

Stream: general

Topic: unknown local constant: _ffresh.0


view this post on Zulip Scott Morrison (Jun 30 2019 at 22:37):

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

view this post on Zulip Simon Hudon (Jun 30 2019 at 22:41):

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

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

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

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