lean-notes

English | 한국어[Korean]

This is a collection of my short Lean code for reference. You are free to reuse the content under the terms of the Apache License, Version 2.0.

I use OmegaT to translate English documentation into Korean. The OmegaT project is in the docs directory. You need to install the Okapi filters plugin for OmegaT to make OmegaT parse Markdown files.

Directories

• Lean code: Notes
  • Anselm: St. Anselm's ontological argument for the existence of God.
  • CategoryMistake: An example of category mistakes.
  • CYSEM: Redefining child or youth sexual exploitation material (CYSEM).
  • PropositionalLogic: A variant of a Hilbert system for intuitionistic propositional logic.
• Documentation: docs
  • English: en
  • Korean: ko