型理論 なんて自分には関係ないと思っているあなたへJun 7, 201326 likes10,243 viewsAI-enhanced description 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.
