型理論 なんて自分には関係ないと思っているあなたへThis document contains definitions and proofs about natural numbers, functions, and theorems in Coq. It defines natural numbers as inductive types, defines addition as a recursive function, and proves theorems like 1+1=2. It also contains definitions for monads and proofs about monad bind being associative in Coq.
