def Qq.Quoted (α : Lean.Expr) : Type

Quoted α is the type of Lean expressions having type α.

You should usually write this using the notation Q($α).

Equations

• Qq.Quoted α = Lean.Expr

Instances For

• Qq.instBEqQuoted
• Qq.instCoeOutQuotedExpr
• Qq.instCoeOutQuotedMessageData
• Qq.instHashableQuoted
• Qq.instInhabitedQuoted
• Qq.instReprQuoted
• Qq.instToMessageDataQuoted
• Qq.instToStringQuoted

def Qq.Quoted.unsafeMk {α : Lean.Expr} (e : Lean.Expr) : Quoted α

Creates a quoted expression. Requires that e has type α.

You should usually write this using the notation q($e).

Equations

• Qq.Quoted.unsafeMk e = e

instance Qq.instBEqQuoted {α : Lean.Expr} : BEq (Quoted α)

Equations

• Qq.instBEqQuoted = inferInstanceAs (BEq Lean.Expr)

instance Qq.instHashableQuoted {α : Lean.Expr} : Hashable (Quoted α)

Equations

• Qq.instHashableQuoted = inferInstanceAs (Hashable Lean.Expr)

instance Qq.instInhabitedQuoted {α : Lean.Expr} : Inhabited (Quoted α)

Equations

• Qq.instInhabitedQuoted = inferInstanceAs (Inhabited Lean.Expr)

instance Qq.instToStringQuoted {α : Lean.Expr} : ToString (Quoted α)

Equations

• Qq.instToStringQuoted = inferInstanceAs (ToString Lean.Expr)

instance Qq.instReprQuoted {α : Lean.Expr} : Repr (Quoted α)

Equations

• Qq.instReprQuoted = inferInstanceAs (Repr Lean.Expr)

instance Qq.instCoeOutQuotedExpr {α : Lean.Expr} : CoeOut (Quoted α) Lean.Expr

Equations

• Qq.instCoeOutQuotedExpr = { coe := fun (e : Qq.Quoted α) => e }

instance Qq.instCoeOutQuotedMessageData {α : Lean.Expr} : CoeOut (Quoted α) Lean.MessageData

Equations

• Qq.instCoeOutQuotedMessageData = { coe := Lean.MessageData.ofExpr }

instance Qq.instToMessageDataQuoted {α : Lean.Expr} : Lean.ToMessageData (Quoted α)

Equations

• Qq.instToMessageDataQuoted = { toMessageData := Lean.MessageData.ofExpr }

@[reducible, inline]

abbrev Qq.Quoted.ty {α : Lean.Expr} (t : Quoted α) : Lean.Expr

Gets the type of a quoted expression.

Equations

• t.ty = α

structure Qq.QuotedDefEq {u : Lean.Level} {α : Quoted (Lean.Expr.sort u)} (lhs rhs : Quoted α) : Prop

QuotedDefEq lhs rhs says that the expressions lhs and rhs are definitionally equal.

You should usually write this using the notation $lhs =Q $rhs.

• unsafeIntro :: (
• )

structure Qq.QuotedLevelDefEq (u v : Lean.Level) : Prop

QuotedLevelDefEq u v says that the levels u and v are definitionally equal.

You should usually write this using the notation $u =QL $v.

• unsafeIntro :: (
• )

def Qq.Quoted.check {α : Lean.Expr} (e : Quoted α) : Lean.MetaM Unit

Check that a term e : Q(α) really has type α.

Equations

• One or more equations did not get rendered due to their size.

def Qq.QuotedDefEq.check {u : Lean.Level} {α : Quoted (Lean.Expr.sort u)} {lhs rhs : Quoted α} (e : QuotedDefEq lhs rhs) : Lean.MetaM Unit

Check that the claim $lhs =Q $rhs is actually true; that the two terms are defeq.

Equations

• One or more equations did not get rendered due to their size.

def Qq.QuotedLevelDefEq.check {lhs rhs : Lean.Level} (e : QuotedLevelDefEq lhs rhs) : Lean.MetaM Unit

Check that the claim $u =QL $v is actually true; that the two levels are defeq.

Equations

• One or more equations did not get rendered due to their size.