Created
March 2, 2025 16:28
-
-
Save park-sewon/d1a4c56b5a39765f37995c717830de36 to your computer and use it in GitHub Desktop.
LEAN tag attribute for checking classical axioms in Prop
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Lean | |
| import Lean.Util.CollectAxioms | |
| open Lean | |
| initialize intuitionisticAttr : TagAttribute ← | |
| registerTagAttribute `intuitionistic "Tag attribute for intuitionistic prop" | |
| fun decl => | |
| do | |
| let axioms ← collectAxioms decl | |
| let invalid_axioms := axioms.filter | |
| fun | `propext | `Quot.sound => false | |
| | x => true | |
| if ! invalid_axioms.isEmpty then | |
| throwError "'{decl}' depends on the following classical axiom(s): {invalid_axioms.qsort Name.lt |>.toList}" | |
| pure () |
Author
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Rejects
@[intuitionistic] theorem a : ...whenais proved depending on axioms other thanpropextorQuot.sound. This attribute cannot be used in the same file.