From 920bdead01153699f78928151547bfbc8aef53ad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Oct 2019 10:45:26 -0700 Subject: [PATCH] chore: add helper functions --- library/Init/Lean/Expr.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean index 11d7211624..3ebea98f3d 100644 --- a/library/Init/Lean/Expr.lean +++ b/library/Init/Lean/Expr.lean @@ -370,6 +370,11 @@ match e with | forallE n bi d b => updateForall (forallE n bi d b) newBinfo newDomain newBody rfl | _ => panic! "forall expected" +@[inline] def updateForallE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr := +match e with +| forallE n bi d b => updateForall (forallE n bi d b) bi newDomain newBody rfl +| _ => panic! "forall expected" + @[extern "lean_expr_update_lambda"] def updateLambda (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isLambda = true) : Expr := lam e.bindingName newBinfo newDomain newBody @@ -379,6 +384,11 @@ match e with | lam n bi d b => updateLambda (lam n bi d b) newBinfo newDomain newBody rfl | _ => panic! "lambda expected" +@[inline] def updateLambdaE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr := +match e with +| lam n bi d b => updateLambda (lam n bi d b) bi newDomain newBody rfl +| _ => panic! "lambda expected" + @[extern "lean_expr_update_let"] def updateLet (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (h : e.isLet = true) : Expr := letE e.letName newType newVal newBody