如何在VS Code的Lean4中查找类型类的实例定义？

安全阿岳

2026-8-6

在VS Code中查找Lean4类型类实例的方法

用命令面板直接搜实例
按下Cmd/Ctrl + Shift + P打开命令面板，输入Lean: Find Instances，接着输入目标类型类名（比如IsCommutative），就能看到所有该类的实例列表，找到对应Or的那条就行。
通过#synth命令跳转
在代码里写#synth IsCommutative Or，执行后按住Cmd/Ctrl点击输出结果里的实例名称，直接跳转到该实例的定义处。另外输入实例代码时，插件的补全提示也能帮你定位到目标实例。
从类定义找引用
先跳转到IsCommutative的类定义，在comm字段上按下Cmd/Ctrl + Shift + F（或者右键选“Find All References”），所有实现该字段的实例都会被列出来，筛选出Or对应的实例即可。