HTPILeanPackage

Open this package in VS Code to write proofs in Lean. The file HTPILib/HTPIDefs.lean defines tactics that are used in How To Prove It With Lean.

Name		Name	Last commit message	Last commit date
Latest commit History 78 Commits
HTPILib		HTPILib
build		build
lake-packages		lake-packages
.gitignore		.gitignore
Blank.lean		Blank.lean
Chap3Ex.lean		Chap3Ex.lean
Chap4Ex.lean		Chap4Ex.lean
Chap5Ex.lean		Chap5Ex.lean
Chap6Ex.lean		Chap6Ex.lean
IntroLean.lean		IntroLean.lean
LICENSE		LICENSE
README.md		README.md
lake-manifest.json		lake-manifest.json
lakefile.lean		lakefile.lean
lean-toolchain		lean-toolchain

Provide feedback