等式证明中的模式匹配解构

问题描述

data T = A String | B String

p : ((A s) = (A s')) -> (s = s')

如果我有 (A s) = (A s')，我如何获得 s = s'？

附言我是伊德里斯的新手。随意编辑我的代码样式问题或添加相关关键字。

解决方法

Refl 上的模式匹配：

data T = A String | B String

p : ((A s) = (A s')) -> (s = s')
p Refl = Refl