def Qq.mkFreshExprMVarQ {u : Lean.Level} (ty : Q(Sort u)) (kind : optParam Lean.MetavarKind Lean.MetavarKind.natural) (userName : optParam 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 α none

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

Equations

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

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 : optParam Bool true) (implicitLambda : optParam Bool true) (errorMsgHeader? : optParam (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(«$α»))

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

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 : Q(«$α»)) (b : Q(«$α»)) : Type

• 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 : Q(«$α»)) (b : Q(«$α»)) : Lean.MetaM (Qq.MaybeDefEq a b)

Equations

• Qq.isDefEqQ a b = do let __do_lift ← Lean.Meta.isDefEq a b if __do_lift = true then pure (Qq.MaybeDefEq.defEq (_ : «$a» =Q «$b»)) else pure Qq.MaybeDefEq.notDefEq

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

Equations

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