$p$-进数的初步单值形式化
逻辑
2013-02-07 v1 计算机科学中的逻辑
摘要
本文在第二作者的单值基础计划背景下，给出了-进数的初步形式化。我们还提供了相应的代码，在证明助手 Coq 中验证了该构造。由于单值设定下的工作正在进行中，随着作者和其他研究人员未来对 Coq 库进行更合适的重排和优化，本文中给出的-进数构造的结构和组织预计会发生变化。因此，我们此处的构造应被视为一个有待改进的初步近似。
引用
@article{arxiv.1302.1207,
title = {A preliminary univalent formalization of the p-adic numbers},
author = {Álvaro Pelayo and Vladimir Voevodsky and Michael A. Warren},
journal= {arXiv preprint arXiv:1302.1207},
year = {2013}
}
备注
57 pages