You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Lean claims to cache the first has_one α instance when elaborating the type of h, but then searches for it again. I'm told this is unexpected and likely a bug ;)
Prerequisites
Put an X between the brackets on this line if you have done all of the following:
Lean claims to cache the first
has_one α
instance when elaborating the type ofh
, but then searches for it again. I'm told this is unexpected and likely a bug ;)Prerequisites
or feature requests.
Description
[Description of the issue]
Steps to Reproduce
Expected behavior: [What you expect to happen]
Actual behavior: [What actually happens]
Reproduces how often: [What percentage of the time does it reproduce?]
Versions
You can get this information from copy and pasting the output of
lean --version
,please include the OS and what version of the OS you're running.
Additional Information
Any additional information, configuration or data that might be necessary to reproduce the issue.
The text was updated successfully, but these errors were encountered: