文件名称：lics2021：Agda开发将支持LICS 2021提交的“具有构造实数的全局优化”
文件大小：27KB
文件格式：ZIP
更新时间：2024-03-02 05:14:51
Agda
具有构造实数的全局优化 这一发展使我们在论文提交中看到的证明形式化。 我们按顺序从纸上遍历每个编号的定义/引理/定理/推论，并给出在代码中将该语句形式化的类型或函数。 关键结果（本文中的定理）以粗体编号，以方便识别。 回想一下，此开发基于MartínEscardó的库，并利用了其许多文件。 II-B节在Codistances.agda文件中Codistances.agda ＃ 正规化 01 在TypeTopology文件Codistance.lagda作为is-codistance 02 未在此仓库中正式化 03 未在此仓库中正式化 04 ×-codistance和×ⁿ-codistance 05 未在此仓库中正式化 06 在TypeTopology文件中，将Codistance.lagda作为codistance 07 在TypeTopology文件中，将Co
【文件预览】：
lics2021-main
----SearchableTypes.agda(6KB)
----IntervalObjectApproximation.agda(9KB)
----SignedDigit.agda(6KB)
----ConvergenceTheorems.agda(14KB)
----Codistances.agda(7KB)
----ESIntervalObject.lagda(29KB)
----SignedDigitIntervalObject.agda(11KB)
----SignedDigitContinuity.agda(13KB)
----Prelude.agda(2KB)
----README.md(3KB)