Agda 等效于`destruct <term> eqn:<identifier>` [重复]答案

【问题标题】：Agda equivalent of `destruct <term> eqn:<identifier>` [duplicate]Agda 等效于`destruct <term> eqn:<identifier>` [重复]
【发布时间】：2020-07-23 18:56:41
【问题描述】：

我知道 Agda 使用 with 子句进行案例分析，这与 Coq 的 destruct 策略类似。 destruct 策略有一个destruct <term> eqn:<identifier> 形式的variant，它在上下文中额外添加了<term> 和<term> 在每种情况下采用的值之间的等式。有没有类似的方法可以在 Agda 中将此等式添加到上下文中？

【问题讨论】：

标签： coq agda

【解决方案1】：

您需要使用 inspect 成语，这将完全满足您的要求。

我已经在下面的答案中详细描述了如何使用它：

`with f x` matches `false`, but cannot construct `f x == false`

【讨论】：