我不太理解“相等性”和“本地定义”的区别。例如,在阅读与
记住term为ident
在 * 中,这将表现为设置(ident := term),并且使用逻辑(莱布尼兹)相等性而不是本地定义。
实际上,
1.
在第二种情况中,我可以使用生成的假设,如
此外,如果两者之间的区别是基本的,为什么在文档(8.5p1)中将
set
策略相关的文档时:记住term为ident
在 * 中,这将表现为设置(ident := term),并且使用逻辑(莱布尼兹)相等性而不是本地定义。
实际上,
1.
set (ca := c + a) in *.
例如,在上下文中生成ca := c + a:Z
,而
2. remember (c + a ) as ca.
会在上下文中生成Heqca : ca = c + a
。在第二种情况中,我可以使用生成的假设,如
rewrite Heqca。
,而在第一种情况中,我不能使用rewrite ca
。那么第1种的用途是什么?在实际使用中它与第2种有何不同?此外,如果两者之间的区别是基本的,为什么在文档(8.5p1)中将
remember
描述为set
的变体?