论文标题
简化铸造和胁迫
Simplifying Casts and Coercions
论文作者
论文摘要
本文介绍了Norm_cast，这是一个策略工具箱，用于精益证明助手，旨在操纵包含胁迫和铸件的表情。这些表达可能会使开始和专家用户都令人沮丧。胁迫的存在可能导致看似相同的表达方式无法统一并重写失败。 Norm_cast策略旨在以透明的表达方式进行推理。它们被广泛用于消除精益数学库和外部发展中的样板参数。
This paper introduces norm_cast, a toolbox of tactics for the Lean proof assistant designed to manipulate expressions containing coercions and casts. These expressions can be frustrating for beginning and expert users alike; the presence of coercions can cause seemingly identical expressions to fail to unify and rewrites to fail. The norm_cast tactics aim to make reasoning with such expressions as transparent as possible. They are used extensively to eliminate boilerplate arguments in the Lean mathematical library and in external developments.
