如何在精益编译时证明关系？

作者: 不浪漫
发布时间: 2025-02-27 06:21:20 (11小时前)
转自：

2 条回复

0#
回复此人
12345 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 你应该可以使用 <code> dec_trivial </code> 证明 <code> l1_sorted </code> 。这将尝试推断出一个实例 <code> decidable (is_sorted l1) </code> ，如果实例的计算结果为 <code> is_true p </code> ，它将减少到 <code> p </code> 。 </p> </DIV>

编辑

登录后才能参与评论