Qq-ified spellings of functions in Lean.Meta

This file provides variants of the function in the Lean.Meta namespace, which operate with Q(_) instead of Expr.

def Qq.mkFreshExprMVarQ {u : Lean.Level} (ty : Q(Sort u)) (kind : Lean.MetavarKind := Lean.MetavarKind.natural) (userName : Lean.Name := Lean.Name.anonymous) : Lean.MetaM Q(«$ty»)

def Qq.withLocalDeclDQ {n : Type → Type u_1} {u : Lean.Level} {α : Type} [Monad n] [MonadControlT Lean.MetaM n] (name : Lean.Name) (β : Q(Sort u)) (k : Q(«$β») → n α) : n α

def Qq.withLocalDeclQ {n : Type → Type u_1} {u : Lean.Level} {α : Type} [Monad n] [MonadControlT Lean.MetaM n] (name : Lean.Name) (bi : Lean.BinderInfo) (β : Q(Sort u)) (k : Q(«$β») → n α) : n α

def Qq.trySynthInstanceQ {u : Lean.Level} (α : Q(Sort u)) : Lean.MetaM (Lean.LOption Q(«$α»))

def Qq.synthInstanceQ {u : Lean.Level} (α : Q(Sort u)) : Lean.MetaM Q(«$α»)

def Qq.instantiateMVarsQ {u : Lean.Level} {α : Q(Sort u)} (e : Q(«$α»)) : Lean.MetaM Q(«$α»)

def Qq.elabTermEnsuringTypeQ {u : Lean.Level} (stx : Lean.Syntax) (expectedType : Q(Sort u)) (catchExPostpone implicitLambda : Bool := true) (errorMsgHeader? : Option String := none) : Lean.Elab.TermElabM Q(«$expectedType»)

def Qq.inferTypeQ (e : Lean.Expr) : Lean.MetaM ((u : Lean.Level) × (α : have u := u; Q(Sort u)) × Q(«$α»))

A Qq-ified version of Lean.Meta.inferType

Instead of writing let α ← inferType e, this allows writing let ⟨u, α, e⟩ ← inferTypeQ e, which results in a context of

e✝ : Expr
u : Level
α : Q(Type u)
e : Q($α)

Here, the new e is defeq to the old one, but now has Qq-ascribed type information.

This is frequently useful when using the ~q matching from QQ/Match.lean, as it allows an Expr to be turned into something that can be matched upon.

def Qq.checkTypeQ {u : Lean.Level} (e : Lean.Expr) (ty : have u := u; Q(Sort u)) : Lean.MetaM (Option Q(«$ty»))

If e is a ty, then view it as a term of Q($ty).

inductive Qq.MaybeDefEq {u : Lean.Level} {α : let u := u; Q(Sort u)} (a b : Q(«$α»)) : Type

The result of Qq.isDefEqQ; MaybeDefEq a b is an optional version of $a =Q $b.

• defEq {u : Lean.Level} {α : let u := u; Q(Sort u)} {a b : Q(«$α»)} : «$a» =Q «$b» → MaybeDefEq a b
• notDefEq {u : Lean.Level} {α : let u := u; Q(Sort u)} {a b : Q(«$α»)} : MaybeDefEq a b

@[implicit_reducible]

instance Qq.instReprMaybeDefEq {u✝ : Lean.Level} {α✝ : have u := u✝; Q(Sort u)} {a b : Q($α✝)} : Repr (MaybeDefEq a b)

def Qq.isDefEqQ {u : Lean.Level} {α : have u := u; Q(Sort u)} (a b : Q(«$α»)) : Lean.MetaM (MaybeDefEq a b)

A version of Lean.Meta.isDefEq which returns a strongly-typed witness rather than a bool.

def Qq.assertDefEqQ {u : Lean.Level} {α : have u := u; Q(Sort u)} (a b : Q(«$α»)) : Lean.MetaM (PLift («$a» =Q «$b»))

Like Qq.isDefEqQ, but throws an error if not defeq.

inductive Qq.MaybeLevelDefEq (u v : Lean.Level) : Type

The result of Qq.isLevelDefEqQ; MaybeLevelDefEq u v is an optional version of $u =QL $v.

• defEq {u v : Lean.Level} : u =QL v → MaybeLevelDefEq u v
• notDefEq {u v : Lean.Level} : MaybeLevelDefEq u v

@[implicit_reducible]

instance Qq.instReprMaybeLevelDefEq {u v : Lean.Level} : Repr (MaybeLevelDefEq u v)

def Qq.isLevelDefEqQ (u v : Lean.Level) : Lean.MetaM (MaybeLevelDefEq u v)

A version of Lean.Meta.isLevelDefEq which returns a strongly-typed witness rather than a bool.

def Qq.assertLevelDefEqQ (u v : Lean.Level) : Lean.MetaM (PLift (u =QL v))

Like Qq.isLevelDefEqQ, but throws an error if not defeq.