我希望伊德里斯证明那里testMult : mult 3 3 = 9
有人居住。
不幸的是,这被键入为
mult (fromInteger 3) (fromInteger 3) = fromInteger 9 : Type
我可以像这样解决它:
n3 : Nat; n3 = 3
n9 : Nat; n9 = 9
testMult : mult n3 n3 = n9
testMult = Refl
有没有办法做类似的事情mult (3 : Nat) (3 : Nat) = (9 : Nat)
?