Zulip Chat Archive

Stream: general

Topic: bug


view this post on Zulip Kenny Lau (Aug 13 2018 at 09:38):

import algebra.module

universes u v w

variables (R : Type u) [comm_ring R] (M : Type v) [module R M]

class A : Prop :=
(A :  N : set M, is_submodule N)

/-
failed to synthesize type class instance for
R : Type u,
_inst_1 : comm_ring R,
M : Type v,
_inst_2 : module R M,
M : Type v,
N : set M
⊢ module ?m_1 M
-/

view this post on Zulip Kenny Lau (Aug 13 2018 at 09:38):

why are there two M : Type v?

view this post on Zulip Mario Carneiro (Aug 13 2018 at 10:08):

yes this is a bug, I think it was reported and I thought it was fixed

view this post on Zulip Mario Carneiro (Aug 13 2018 at 10:10):

if you put (M : Type v) [module R M] in the class definition it works


Last updated: May 15 2021 at 00:39 UTC