以下代码有一个奇怪的行为
变量(toto:Type)检查eq.symm –output:eq.symm:?toto =?btoto ?b toto =?a toto我希望检查不考虑不相关的……
我得到了答案 github问题在这里 。
这实际上是一个引用的bug 这里 这可以通过做任何一种来解决
print eq.symm -- theorem eq.symm : ? {A : Type} {a b : A}, a = b �� b = a := -- �� A a, eq.rec (eq.refl a) check @eq.symm -- eq.symm : ? {A} {a b}, a = b �� b = a