Zulip Chat Archive

Stream: general

Topic: Lean being stubborn with class instances


view this post on Zulip Kenny Lau (Jul 16 2019 at 08:41):

import linear_algebra.basic

#check λ f : ( : ideal ) [] ( : ideal ), f 0
-- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

view this post on Zulip Kenny Lau (Jul 16 2019 at 08:42):

I think the cause is the fact that the ideal is a module over Z in two ways

view this post on Zulip Kenny Lau (Jul 16 2019 at 08:42):

in f, the module instance is the second one

view this post on Zulip Kenny Lau (Jul 16 2019 at 08:42):

but when I want to coerce f to a function, Lean can only deal with the first one

view this post on Zulip Kenny Lau (Jul 16 2019 at 08:43):

despite the fact that the module instances is already encoded in the type of f...


Last updated: May 09 2021 at 18:17 UTC