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)

Equations

• { ty := none, fvarId := fvarId, userName := userName }.fvarTy = q(Lean.Level)
• { ty := some val, fvarId := fvarId, userName := userName }.fvarTy = q(Lean.Expr)

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

Equations

• decl.fvar = Lean.Expr.fvar decl.fvarId

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

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.mkIsDefEqType [] = q(Bool)

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)

Equations

• Qq.Impl.mkIsDefEqResultVal [] val = q(«$val»)
• Qq.Impl.mkIsDefEqResultVal ({ ty := none, fvarId := fvarId, userName := userName } :: decls) val = Qq.Impl.mkIsDefEqResultVal decls q(«$val».snd)
• Qq.Impl.mkIsDefEqResultVal ({ ty := some val_1, fvarId := fvarId, userName := userName } :: decls) val = Qq.Impl.mkIsDefEqResultVal decls q(«$val».snd)

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

Equations

• Qq.Impl.mkLambda' n fvar ty body = do let __do_lift ← body.abstractM #[fvar] pure (Lean.mkLambda n Lean.BinderInfo.default ty __do_lift)

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

Equations

• Qq.Impl.mkLet' n fvar ty val body = do let __do_lift ← body.abstractM #[fvar] pure (Lean.mkLet n ty val __do_lift)