## Stream: general

### Topic: Lean being stubborn with class instances

#### 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')


#### 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

#### Kenny Lau (Jul 16 2019 at 08:42):

in f, the module instance is the second one

#### 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

#### 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