如何强制在lean4中使用类型类的实例？

Question

我试图学习精益，我不小心将 concatenate_junk 类型输入保留为 ˋStringˋ 而不是 ˋaˋ。

class ConcatenateJunk (a: Type u) where
  concatenate_junk: String -> String

instance: ConcatenateJunk String where
  concatenate_junk := λ x => x

instance: ConcatenateJunk Nat where
  concatenate_junk := λ x => "junk" ++ toString x

#eval ConcatenateJunk.concatenate_junk 42

这让我思考：如何调用

ConcatenateJunk.concatenate_junk

来实例化 Nat？由于“concatenate_junk”中没有类型参数，编译器不知道选择哪个实例。

如何选择？

Answer 1

我想你的意思是：

class ConcatenateJunk (a: Type u) where
  concatenate_junk: a -> String  -- this line has changed

instance: ConcatenateJunk String where
  concatenate_junk := λ x => x

instance: ConcatenateJunk Nat where
  concatenate_junk := λ x => "junk" ++ toString x

#eval ConcatenateJunk.concatenate_junk 42

您的第一个

String

应该是

a

。