max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add helper functions

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-25 10:45:26 -07:00
parent 2eeeab68b3
commit 920bdead01
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/Init/Lean/Expr.lean
View file

@ -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