常用数学知识

hexo deploy时TypeError [ERR_INVALID_ARG_TYPE]解决

Coq IDE Unset Printing Notations问题

给手机换个屏幕

在arm架构系统中用qemu运行x86-64程序

k3s搭建

$\lambda$表达式中的$\alpha$-转换

CentOs虚拟机折腾k8s

coq中几种cbv归约方式

记一次用verilog设计CPU踩的坑