加载中…
2013-12-30
Experimental library of univalent formalization of mathematics
Vladimir Voevodsky
文献摘要
This paper contains a discussion of a library of formalized mathematics for the proof assistant Coq which the author worked on in 2011-13.
讨论
0讲解博客
生成讲解博客的中文版本
AI智能校验
生成AI智能校验的中文版本