phanerozoic/

Lean4-Qq

Qq provides type-safe expression quotations for constructing object-level expressions in meta-level Lean 4 code.

Repository: https://github.com/leanprover-community/quote4 Commit: 8d33324ee877e9735d2829bc6f1f439e60cf98b1 Files: 28 License: apache-2.0

	Schema




	

Column Type Description

statement string Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof

proof… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Lean4-Qq.