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

chore: move to new frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-17 07:40:34 -07:00
parent 0472f38dc8
commit 4925bf22d4
2 changed files with 19 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/Tactic/FVarSubst.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -8,8 +9,7 @@ import Lean.Expr
import Lean.LocalContext
import Lean.Util.ReplaceExpr
namespace Lean
namespace Meta
namespace Lean.Meta
/-
Some tactics substitute hypotheses with expressions.
We track these substitutions using `FVarSubst`.

35
src/Lean/Meta/Tactic/Generalize.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -6,25 +7,23 @@ Authors: Leonardo de Moura
import Lean.Meta.KAbstract
import Lean.Meta.Tactic.Util
namespace Lean
namespace Meta
namespace Lean.Meta
def generalize (mvarId : MVarId) (e : Expr) (x : Name) (failIfNotInTarget : Bool := true) : MetaM MVarId := do
withMVarContext mvarId $ do
checkNotAssigned mvarId `generalize;
tag ← getMVarTag mvarId;
target ← getMVarType mvarId;
target ← instantiateMVars target;
targetAbst ← kabstract target e;
when (failIfNotInTarget && !targetAbst.hasLooseBVars) $
throwTacticEx `generalize mvarId ("failed to find expression in the target");
eType ← inferType e;
let targetNew := Lean.mkForall x BinderInfo.default eType targetAbst;
unlessM (isTypeCorrect targetNew) $
throwTacticEx `generalize mvarId ("result is not type correct");
mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag;
assignExprMVar mvarId (mkApp mvarNew e);
withMVarContext mvarId do
checkNotAssigned mvarId `generalize
let tag ← getMVarTag mvarId
let target ← getMVarType mvarId
let target ← instantiateMVars target
let targetAbst ← kabstract target e
if failIfNotInTarget && !targetAbst.hasLooseBVars then
throwTacticEx `generalize mvarId "failed to find expression in the target"
let eType ← inferType e
let targetNew := Lean.mkForall x BinderInfo.default eType targetAbst
unless (← isTypeCorrect targetNew) do
throwTacticEx `generalize mvarId "result is not type correct"
let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag
assignExprMVar mvarId (mkApp mvarNew e)
pure mvarNew.mvarId!
end Meta
end Lean
end Lean.Meta