Documentation

Lean.Elab.Tactic.CbvSimproc

source
def Lean.Elab.elabCbvSimprocPattern (stx : Syntax) :
MetaM Expr
Instances For
    source
    def Lean.Elab.mkSimprocPatternFromExpr (e : Expr) :
    MetaM Meta.Sym.Pattern
    Instances For
      source
      def Lean.Elab.elabCbvSimprocKeys (stx : Syntax) :
      MetaM (Array Meta.DiscrTree.Key)
      Instances For
        source
        def Lean.Elab.checkCbvSimprocType (declName : Name) :
        CoreM Unit
        Instances For
          source
          def Lean.Elab.Command.elabCbvSimprocPattern :
          CommandElab
          Instances For
            source
            def Lean.Elab.Command.elabCbvSimprocPatternBuiltin :
            CommandElab
            Instances For