Documentation

Mathlib.Tactic.ToExpr

ToExpr instances for Mathlib #

source
def Mathlib.instToExprULift_mathlib.toExpr {α✝ : Type s} [Lean.ToExpr α✝] :
Lean.ToLevel → Lean.ToLevel → ULift α✝ → Lean.Expr
Instances For
    source
    @[implicit_reducible]
    instance Mathlib.instToExprULift_mathlib {α✝ : Type s} [Lean.ToExpr α✝] [Lean.ToLevel] [Lean.ToLevel] :
    Lean.ToExpr (ULift α✝)
    source
    @[implicit_reducible]
    instance Mathlib.instToExprPUnitOfToLevel_mathlib [Lean.ToLevel] :
    Lean.ToExpr PUnit

    Hand-written instance since PUnit is a Sort rather than a Type.

    source
    @[implicit_reducible]
    instance Mathlib.instToExprRaw_mathlib :
    Lean.ToExpr String.Pos.Raw
    source
    def Mathlib.instToExprRaw_mathlib.toExpr :
    String.Pos.Raw → Lean.Expr
    Instances For
      source
      @[implicit_reducible]
      instance Mathlib.instToExprRaw_mathlib_1 :
      Lean.ToExpr Substring.Raw
      source
      def Mathlib.instToExprRaw_mathlib_1.toExpr :
      Substring.Raw → Lean.Expr
      Instances For
        source
        def Mathlib.instToExprSourceInfo_mathlib.toExpr :
        Lean.SourceInfo → Lean.Expr
        Instances For
          source
          @[implicit_reducible]
          instance Mathlib.instToExprSourceInfo_mathlib :
          Lean.ToExpr Lean.SourceInfo
          source
          partial def Mathlib.instToExprSyntax_mathlib.toExpr :
          Lean.Syntax → Lean.Expr
          source
          @[implicit_reducible]
          instance Mathlib.instToExprSyntax_mathlib :
          Lean.ToExpr Lean.Syntax
          source
          @[implicit_reducible]
          instance Mathlib.instToExprMData_mathlib :
          Lean.ToExpr Lean.MData
          source
          def Mathlib.instToExprMVarId_mathlib.toExpr :
          Lean.MVarId → Lean.Expr
          Instances For
            source
            @[implicit_reducible]
            instance Mathlib.instToExprMVarId_mathlib :
            Lean.ToExpr Lean.MVarId
            source
            @[implicit_reducible]
            instance Mathlib.instToExprLevelMVarId_mathlib :
            Lean.ToExpr Lean.LevelMVarId
            source
            def Mathlib.instToExprLevelMVarId_mathlib.toExpr :
            Lean.LevelMVarId → Lean.Expr
            Instances For
              source
              @[implicit_reducible]
              instance Mathlib.instToExprLevel_mathlib :
              Lean.ToExpr Lean.Level
              source
              def Mathlib.instToExprLevel_mathlib.toExpr :
              Lean.Level → Lean.Expr
              Instances For
                source
                @[implicit_reducible]
                instance Mathlib.instToExprBinderInfo_mathlib :
                Lean.ToExpr Lean.BinderInfo
                source
                def Mathlib.instToExprBinderInfo_mathlib.toExpr :
                Lean.BinderInfo → Lean.Expr
                Instances For
                  source
                  def Mathlib.instToExprExpr_mathlib.toExpr :
                  Lean.Expr → Lean.Expr
                  Instances For
                    source
                    @[implicit_reducible]
                    instance Mathlib.instToExprExpr_mathlib :
                    Lean.ToExpr Lean.Expr