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

chore: remove unnecessary method

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-28 05:40:03 -08:00
parent deacb03802
commit 2733a5bebd
1 changed files with 3 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Lean/Meta/Basic.lean
View file

@ -204,14 +204,11 @@ do s ← get;
modify $ fun s => { ngen := s.ngen.next, .. s };
pure id
def mkFreshExprMVarAt (lctx : LocalContext) (type : Expr) (userName : Name := Name.anonymous) (synthetic : Bool := false) : MetaM Expr :=
do mvarId ← mkFreshId;
modify $ fun s => { mctx := s.mctx.addExprMVarDecl mvarId userName lctx type synthetic, .. s };
pure $ mkMVar mvarId
def mkFreshExprMVar (type : Expr) (userName : Name := Name.anonymous) (synthetic : Bool := false) : MetaM Expr :=
do lctx ← getLCtx;
mkFreshExprMVarAt lctx type userName synthetic
mvarId ← mkFreshId;
modify $ fun s => { mctx := s.mctx.addExprMVarDecl mvarId userName lctx type synthetic, .. s };
pure $ mkMVar mvarId
def mkFreshLevelMVar : MetaM Level :=
do mvarId ← mkFreshId;