def Qq.withLetDeclQ {n : Type → Type} {u : Lean.Level} {α : Type} [Monad n] [MonadControlT Lean.MetaM n] (name : Lean.Name) (type : Q(Sort u)) (val : Q(«$type»)) (k : (v : Q(«$type»)) → «$v» =Q «$val» → n α) (nondep : Bool := false) (kind : Lean.LocalDeclKind := Lean.LocalDeclKind.default) : n α

Equations

• Qq.withLetDeclQ name type val k nondep kind = Lean.Meta.withLetDecl name type val (fun (x : Lean.Expr) => k x ⋯) nondep kind

def Qq.mkLetFVarsQ {u : Lean.Level} {T : Q(Sort u)} (xs : Array Lean.Expr) (e : Q(«$T»)) (usedLetOnly generalizeNondepLet : Bool := true) (binderInfoForMVars : Lean.BinderInfo := Lean.BinderInfo.implicit) : Lean.MetaM Q(«$T»)

Equations

• Qq.mkLetFVarsQ xs e usedLetOnly generalizeNondepLet binderInfoForMVars = Lean.Meta.mkLetFVars xs e usedLetOnly generalizeNondepLet binderInfoForMVars

def SynthLean.equateNat (n m : Q(Nat)) : Lean.MetaM Q(«$n» = «$m»)

Equations

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

def SynthLean.ltNat (n m : Q(Nat)) : Lean.MetaM Q(«$n» < «$m»)

Equations

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