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

Equations

• Qq.mkFreshExprMVarQ ty kind userName = Lean.Meta.mkFreshExprMVar (some ty) kind userName

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 α

Equations

• Qq.withLocalDeclDQ name β k = Lean.Meta.withLocalDeclD name β k

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 α

Equations

• Qq.withLocalDeclQ name bi β k = Lean.Meta.withLocalDecl name bi β k

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

Equations

• Qq.trySynthInstanceQ α = Lean.Meta.trySynthInstance α

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

Equations

• Qq.synthInstanceQ α = Lean.Meta.synthInstance α

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

Equations

• Qq.instantiateMVarsQ e = Lean.instantiateMVars e

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

Equations

• Qq.elabTermEnsuringTypeQ stx expectedType catchExPostpone implicitLambda errorMsgHeader? = Lean.Elab.Term.elabTermEnsuringType stx (some expectedType) catchExPostpone implicitLambda errorMsgHeader?

def Qq.inferTypeQ (e : Lean.Expr) : Lean.MetaM ((u : Lean.Level) × (α : let 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.

Equations

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

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

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

Equations

• Qq.checkTypeQ e ty = do let __do_lift ← Lean.Meta.inferType e let __do_lift ← Lean.Meta.isDefEq __do_lift ty if __do_lift = true then pure (some e) else pure none

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» → Qq.MaybeDefEq a b
• notDefEq: {u : Lean.Level} → {α : let u := u; Q(Sort u)} → {a b : Q(«$α»)} → Qq.MaybeDefEq a b

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

Equations

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

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

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

Equations

• Qq.isDefEqQ a b = do let __do_lift ← Lean.Meta.isDefEq a b if __do_lift = true then pure (Qq.MaybeDefEq.defEq ⋯) else pure Qq.MaybeDefEq.notDefEq

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

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

Equations

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