Documentation

Mathlib.Tactic.ToExpr

ToExpr instances for Mathlib #

source
instance Mathlib.instToExprULiftOfToLevel_mathlib {α✝ : Type s} [Lean.ToExpr α✝] [Lean.ToLevel] [Lean.ToLevel] :
Lean.ToExpr (ULift α✝)
Equations
    source
    instance Mathlib.instToExprPUnitOfToLevel_mathlib [Lean.ToLevel] :
    Lean.ToExpr PUnit

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

    Equations
      source
      instance Mathlib.instToExprPos_mathlib :
      Lean.ToExpr String.Pos
      Equations
        source
        instance Mathlib.instToExprSubstring_mathlib :
        Lean.ToExpr Substring
        Equations
          source
          instance Mathlib.instToExprSourceInfo_mathlib :
          Lean.ToExpr Lean.SourceInfo
          Equations
            source
            instance Mathlib.instToExprSyntax_mathlib :
            Lean.ToExpr Lean.Syntax
            Equations
              source
              instance Mathlib.instToExprMData_mathlib :
              Lean.ToExpr Lean.MData
              Equations
                source
                instance Mathlib.instToExprMVarId_mathlib :
                Lean.ToExpr Lean.MVarId
                Equations
                  source
                  instance Mathlib.instToExprLevelMVarId_mathlib :
                  Lean.ToExpr Lean.LevelMVarId
                  Equations
                    source
                    instance Mathlib.instToExprLevel_mathlib :
                    Lean.ToExpr Lean.Level
                    Equations
                      source
                      instance Mathlib.instToExprBinderInfo_mathlib :
                      Lean.ToExpr Lean.BinderInfo
                      Equations
                        source
                        instance Mathlib.instToExprExpr_mathlib :
                        Lean.ToExpr Lean.Expr
                        Equations