@[implicit_reducible]

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

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

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

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).

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[reducible, inline]

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

Gets the type of a quoted expression.

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 α.

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.

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.