LoL : Lots of Logic

This repository is my proof pool.
My environment is WSL: Ubuntu-20.04, Windows 10.

Main Goals = `0 / 6`

Domain Theory (Complete Partial Order, Complete Lattice)
Set Theory (Aczel Tree)
Propositional Logic (Soundness, Completeness)
Simply Typed Lambda Calculus (SN property)
First-Order Logic (Soundness, Completeness)
The Godel's Incompleteness Theorem (1st Thm)

Quick Start

eval `opam env`
coq_makefile -f _CoqProject -o Makefile
make -j4 -k

`coqc -v`

The Coq Proof Assistant, version 8.18.0
compiled with OCaml 5.1.1

Thanks To

References