我试图证明以下内容:
1-pow : ? {n : ?} ? 1 pow n ? 1
1-pow {zero} = refl
1-pow {suc x} = {!!}
我是Adga的新手,甚至不知道从哪里开始.有什么建议或指导吗？显然很容易在纸上证明,但我不确定告诉Agda什么.
我将pow功能定义如下:
_pow_ : ? ? ? ? ?
x pow zero = 1
x pow (suc zero) = x
x pow (suc y) = x * (x pow y)