From 0092c40ce4108a2724df7dd4e4fa3404a7313166 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Feb 2020 08:38:37 -0800 Subject: [PATCH] refactor: make it clear the result are free variables --- src/Init/Lean/Meta/Tactic/Intro.lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/Init/Lean/Meta/Tactic/Intro.lean b/src/Init/Lean/Meta/Tactic/Intro.lean index 08233df1bf..5dcb20729e 100644 --- a/src/Init/Lean/Meta/Tactic/Intro.lean +++ b/src/Init/Lean/Meta/Tactic/Intro.lean @@ -49,27 +49,28 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ else throwTacticEx `introN mvarId "insufficient number of binders" -@[specialize] def introNCore {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → Name × σ) (s : σ) : MetaM (Array Expr × MVarId) := +@[specialize] def introNCore {σ} (mvarId : MVarId) (n : Nat) (mkName : LocalContext → Name → σ → Name × σ) (s : σ) : MetaM (Array FVarId × MVarId) := withMVarContext mvarId $ do checkNotAssigned mvarId `introN; mvarType ← getMVarType mvarId; lctx ← getLCtx; - introNCoreAux mvarId mkName n lctx #[] 0 s mvarType + (fvars, mvarId) ← introNCoreAux mvarId mkName n lctx #[] 0 s mvarType; + pure (fvars.map Expr.fvarId!, mvarId) def mkAuxName (lctx : LocalContext) (defaultName : Name) : List Name → Name × List Name | [] => (lctx.getUnusedName defaultName, []) | n :: rest => (if n == "_" then lctx.getUnusedName defaultName else n, rest) -def introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) : MetaM (Array Expr × MVarId) := +def introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) : MetaM (Array FVarId × MVarId) := introNCore mvarId n mkAuxName givenNames -def intro (mvarId : MVarId) (name : Name) : MetaM (Expr × MVarId) := do -(fvars, mvarId) ← introN mvarId 1 [name]; -pure (fvars.get! 0, mvarId) +def intro (mvarId : MVarId) (name : Name) : MetaM (FVarId × MVarId) := do +(fvarIds, mvarId) ← introN mvarId 1 [name]; +pure (fvarIds.get! 0, mvarId) -def intro1 (mvarId : MVarId) : MetaM (Expr × MVarId) := do -(fvars, mvarId) ← introN mvarId 1 []; -pure (fvars.get! 0, mvarId) +def intro1 (mvarId : MVarId) : MetaM (FVarId × MVarId) := do +(fvarIds, mvarId) ← introN mvarId 1 []; +pure (fvarIds.get! 0, mvarId) end Meta end Lean