相等证明中的模式匹配（解构）

【问题标题】：Pattern-match (destructure) in equality proof相等证明中的模式匹配（解构）
【发布时间】：2021-04-14 15:58:27
【问题描述】：

data T = A String | B String

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

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

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

【问题讨论】：

标签： idris

【解决方案1】：

Refl 上的模式匹配：

data T = A String | B String

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

【讨论】：