Lean.ToExpr

We use the ToExpr type class to convert values of type α into expressions that denote these values in Lean.

Examples:

toExpr true = .const ``Bool.true []

toTypeExpr Bool = .const ``Bool []

See also ToLevel for representing universe levels as Level expressions.

toExpr : α → Expr
Convert a value a : α into an expression that denotes a
toTypeExpr : Expr
Expression representing the type α

Instances

source

@[implicit_reducible]

instance Lean.instToExprNat :

ToExpr Nat

source

@[implicit_reducible]

instance Lean.instToExprInt :

ToExpr Int

source

def Lean.instToExprInt.mkNat (n : Nat) :

Expr

Instances For

source

@[implicit_reducible]

instance Lean.instToExprRat :

ToExpr Rat

source

def Lean.instToExprRat.mkInt (i : Int) :

Expr

Instances For

source

def Lean.instToExprRat.mkNat (n : Nat) :

Expr

Instances For

source

@[implicit_reducible]

instance Lean.instToExprFin {n : Nat} :

ToExpr (Fin n)

source

@[implicit_reducible]

instance Lean.instToExprBitVec {n : Nat} :

ToExpr (BitVec n)

source

@[implicit_reducible]

instance Lean.instToExprUInt8 :

ToExpr UInt8

source

@[implicit_reducible]

instance Lean.instToExprUInt16 :

ToExpr UInt16

source

@[implicit_reducible]

instance Lean.instToExprUInt32 :

ToExpr UInt32

source

@[implicit_reducible]

instance Lean.instToExprUInt64 :

ToExpr UInt64

source

@[implicit_reducible]

instance Lean.instToExprUSize :

ToExpr USize

source

@[implicit_reducible]

instance Lean.instToExprInt8 :

ToExpr Int8

source

def Lean.instToExprInt8.mkNat (n : Nat) :

Expr

Instances For

source

@[implicit_reducible]

instance Lean.instToExprInt16 :

ToExpr Int16

source

def Lean.instToExprInt16.mkNat (n : Nat) :

Expr

Instances For

source

@[implicit_reducible]

instance Lean.instToExprInt32 :

ToExpr Int32

source

def Lean.instToExprInt32.mkNat (n : Nat) :

Expr

Instances For

source

@[implicit_reducible]

instance Lean.instToExprInt64 :

ToExpr Int64

source

def Lean.instToExprInt64.mkNat (n : Nat) :

Expr

Instances For

source

@[implicit_reducible]

instance Lean.instToExprISize :

ToExpr ISize

source

def Lean.instToExprISize.mkNat (n : Nat) :

Expr

Instances For

source

@[implicit_reducible]

instance Lean.instToExprBool :

ToExpr Bool

source

@[implicit_reducible]

instance Lean.instToExprChar :

ToExpr Char

source

@[implicit_reducible]

instance Lean.instToExprString :

ToExpr String

source

@[implicit_reducible]

instance Lean.instToExprUnit :

ToExpr Unit

source

@[implicit_reducible]

instance Lean.instToExprFilePath :

ToExpr System.FilePath

source

@[implicit_reducible]

instance Lean.instToExprName :

ToExpr Name

source

@[implicit_reducible]

instance Lean.instToExprOptionOfToLevel {α : Type u} [ToLevel] [ToExpr α] :

ToExpr (Option α)

source

@[implicit_reducible]

instance Lean.instToExprListOfToLevel {α : Type u} [ToLevel] [ToExpr α] :

ToExpr (List α)

source

@[implicit_reducible]

instance Lean.instToExprArrayOfToLevel {α : Type u} [ToLevel] [ToExpr α] :

ToExpr (Array α)

source

@[implicit_reducible]

instance Lean.instToExprProdOfToLevel {α : Type u} {β : Type v} [ToLevel] [ToLevel] [ToExpr α] [ToExpr β] :

ToExpr (α × β)

source

@[implicit_reducible]

instance Lean.instToExprLiteral :

ToExpr Literal

source

@[implicit_reducible]

instance Lean.instToExprFVarId :

ToExpr FVarId

source

@[implicit_reducible]

instance Lean.instToExprPreresolved :

ToExpr Syntax.Preresolved