Documentation

Lean.Elab.Tactic.Simproc

source
def Lean.Elab.elabSimprocPattern (stx : Syntax) :
MetaM Expr
Instances For
    source
    def Lean.Elab.elabSimprocKeys (stx : Syntax) :
    MetaM (Array Meta.SimpTheoremKey)
    Instances For
      source
      def Lean.Elab.checkSimprocType (declName : Name) :
      CoreM Bool
      Instances For
        source
        def Lean.Elab.Command.elabSimprocPattern :
        CommandElab
        Instances For
          source
          def Lean.Elab.Command.elabSimprocPatternBuiltin :
          CommandElab
          Instances For