Documentation

Lean.Elab.ConfigEval.MetaInstances

Derived evaluator instances for built-in Meta types #

source
def Lean.Elab.ConfigEval.instEvalExprApplyNewGoals.evalExpr :
Expr → MetaM Meta.ApplyNewGoals
Instances For
    source
    def Lean.Elab.ConfigEval.instEvalTermApplyNewGoals.evalTerm :
    Term → TermElabM (Meta.ApplyNewGoals × Expr)
    Instances For
      source
      @[implicit_reducible]
      instance Lean.Elab.ConfigEval.instEvalExprApplyNewGoals :
      EvalExpr Meta.ApplyNewGoals
      source
      @[implicit_reducible]
      instance Lean.Elab.ConfigEval.instEvalTermApplyNewGoals :
      EvalTerm Meta.ApplyNewGoals
      source
      def Lean.Elab.ConfigEval.instEvalTermEtaStructMode.evalTerm :
      Term → TermElabM (Meta.EtaStructMode × Expr)
      Instances For
        source
        @[implicit_reducible]
        instance Lean.Elab.ConfigEval.instEvalTermEtaStructMode :
        EvalTerm Meta.EtaStructMode
        source
        def Lean.Elab.ConfigEval.instEvalExprEtaStructMode.evalExpr :
        Expr → MetaM Meta.EtaStructMode
        Instances For
          source
          @[implicit_reducible]
          instance Lean.Elab.ConfigEval.instEvalExprEtaStructMode :
          EvalExpr Meta.EtaStructMode
          source
          @[implicit_reducible]
          instance Lean.Elab.ConfigEval.instEvalTermTransparencyMode :
          EvalTerm Meta.TransparencyMode
          source
          def Lean.Elab.ConfigEval.instEvalExprTransparencyMode.evalExpr :
          Expr → MetaM Meta.TransparencyMode
          Instances For
            source
            @[implicit_reducible]
            instance Lean.Elab.ConfigEval.instEvalExprTransparencyMode :
            EvalExpr Meta.TransparencyMode
            source
            def Lean.Elab.ConfigEval.instEvalTermTransparencyMode.evalTerm :
            Term → TermElabM (Meta.TransparencyMode × Expr)
            Instances For
              source
              @[implicit_reducible]
              instance Lean.Elab.ConfigEval.instEvalTermOccurrences :
              EvalTerm Meta.Occurrences
              source
              def Lean.Elab.ConfigEval.instEvalTermOccurrences.evalTerm :
              Term → TermElabM (Meta.Occurrences × Expr)
              Instances For
                source
                @[implicit_reducible]
                instance Lean.Elab.ConfigEval.instEvalExprOccurrences :
                EvalExpr Meta.Occurrences
                source
                def Lean.Elab.ConfigEval.instEvalExprOccurrences.evalExpr :
                Expr → MetaM Meta.Occurrences
                Instances For