partial def Lean.Syntax.stripPos : Syntax → Syntax

structure Qq.Impl.PatVarDecl : Type

• ty : Option Q(Lean.Expr)
• fvarId : Lean.FVarId
• userName : Lean.Name

def Qq.Impl.PatVarDecl.fvarTy : PatVarDecl → Q(Type)

def Qq.Impl.PatVarDecl.fvar (decl : PatVarDecl) : have a := decl.fvarTy; Q(«$a»)

def Qq.Impl.mkIsDefEqType : List PatVarDecl → Q(Type)

def Qq.Impl.mkIsDefEqResult (val : Bool) (decls : List PatVarDecl) : have a := mkIsDefEqType decls; Q(«$a»)

def Qq.Impl.mkIsDefEqResultVal (decls : List PatVarDecl) : (have a := mkIsDefEqType decls; Q(«$a»)) → Q(Bool)

def Qq.Impl.mkLambda' (n : Lean.Name) (fvar ty body : Lean.Expr) : Lean.MetaM Lean.Expr

def Qq.Impl.mkLet' (n : Lean.Name) (fvar ty val body : Lean.Expr) : Lean.MetaM Lean.Expr