LEAN tag attribute for checking classical axioms in Prop

IntuitionisticAttr.lean

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 ()

Rejects @[intuitionistic] theorem a : ... when a is proved depending on axioms other than propext or Quot.sound. This attribute cannot be used in the same file.