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

feat: add assertExt

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-07 12:06:53 -07:00
parent feda5e746f
commit c59fda4c19
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Lean/Meta/Tactic/Assert.lean
View file

@ -34,5 +34,21 @@ withMVarContext mvarId $ do
assignExprMVar mvarId newMVar;
pure newMVar.mvarId!
/--
Convert the given goal `Ctx |- target` into `Ctx |- forall (name : type) -> name = val -> target`.
It assumes `val` has type `type` -/
def assertExt (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) (hName : Name := `h) : MetaM MVarId := do
withMVarContext mvarId $ do
checkNotAssigned mvarId `assert;
tag ← getMVarTag mvarId;
target ← getMVarType mvarId;
u ← getLevel type;
let hType := mkApp3 (mkConst `Eq [u]) type (mkBVar 0) val;
let newType := Lean.mkForall name BinderInfo.default type $ Lean.mkForall hName BinderInfo.default hType target;
newMVar ← mkFreshExprSyntheticOpaqueMVar newType tag;
rflPrf ← mkEqRefl val;
assignExprMVar mvarId (mkApp2 newMVar val rflPrf);
pure newMVar.mvarId!
end Meta
end Lean