Zulip Chat Archive
Stream: mathlib4
Topic: Dangerous instances in !4#2127
Arien Malec (Feb 07 2023 at 04:40):
Could I ask someone to look at !4#2127, line 115?
I'm getting a dangerousInstance lint that I don't know how to fix.
Last updated: Dec 20 2023 at 11:08 UTC