Understanding Fix_eq in Coq

The problemWhen we try to prove that one general recursion defined in coq is actually correct, in the sense that the fixpoint gives exact the same result if we unfold it once. In words of Coq, it is 1

Understanding Number Representation System

There is two well-known number representation in computer: one’s complement and two’s complement. While the latter one is widely adopted almost everywhere in the computer, the former one is still used

Reasoning about programs

Summary of last yearIt has been quite a long time since my last post (which is also unfinished). Lots of things has happened and changed since last blog. I’ve been interning at Apple through the end o

Web front-end Learning notes

Realizing that I’m too weak in the front-end and lack practice. I’m determined to start to write a SPA this winter holiday. This post is intended to note down some discoveries during development. Meta

Fedora configuration

This is only notes for myself. Not the best practice and not for anyone else. PreconfigurationInstall fedy as soon as possible, which save you of a lot of troubles.1bash -c 'su -c "curl http://folkswi

Vagrant and Virtualbox

Notes only, not best practice Mount protocol error1sudo ln -s /opt/VBoxGuestAdditions-*/lib/VBoxGuestAdditions /usr/lib/VBoxGuestAdditions Mount: No such devicestart the virtual machine in the virtual

iptables and firewalld tricks

CauseSome libev port version of something does not support the --forbidden-ip option. To avoid SMTP abuse, originally I moved back to the python version of it. Later I found python version has some bu


期末考完一塌糊涂于是开始埋头写代码 正好pm iceboy开始了vj4项目,就顺便学习一下python好了 Day 0今天装好了系统,不过感觉centos真不友好,各种版本低全部要自己编译安装,还是fedora大法好。 装了一个velocity看起来挺好用的,本来以为只有查看api的功能,结果发现tornado的整个readthedoc都被缓存下来,可以直接看教程。 热烈盼望换上mbp就能有das

LaTeX and more

ShareLaTeX Predifitions and Macros Commonly used tricks Since LaTeX is recommanded in VV186 and many other courses and LaTeX is unfriendly to newbies, I’m going to share my LaTeX writing style. Sh