Documentation

Mathlib.Tactic.ToExpr

ToExpr instances for Mathlib #

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

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

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