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

refactor: move mkArrow to CoreM

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-10 20:15:38 -07:00
parent d61b8fc68d
commit 52f3a3ff2c
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/CoreM.lean
View file

@ -263,4 +263,8 @@ def Exception.isMaxHeartbeat (ex : Exception) : Bool :=
| Exception.error _ (MessageData.ofFormat (Std.Format.text msg)) => "(deterministic) timeout".isPrefixOf msg
| _ => false
/-- Creates the expression `d → b` -/
def mkArrow (d b : Expr) : CoreM Expr :=
return Lean.mkForall (← mkFreshUserName `x) BinderInfo.default d b
end Lean

4
src/Lean/Meta/Basic.lean
View file

@ -774,10 +774,6 @@ def mkLambdaFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedL
def mkLetFVars (xs : Array Expr) (e : Expr) (usedLetOnly := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr :=
mkLambdaFVars xs e (usedLetOnly := usedLetOnly) (binderInfoForMVars := binderInfoForMVars)
/-- Creates the expression `d → b` -/
def mkArrow (d b : Expr) : MetaM Expr :=
return Lean.mkForall (← mkFreshUserName `x) BinderInfo.default d b
/-- `fun _ : Unit => a` -/
def mkFunUnit (a : Expr) : MetaM Expr :=
return Lean.mkLambda (← mkFreshUserName `x) BinderInfo.default (mkConst ``Unit) a