From 77eba18c8b6cff767c97af4522fd6888718bf2ee Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 10 Apr 2024 14:15:02 +0200 Subject: [PATCH 1/3] doc: instantiateMVars (unclear if the example is worth the hover space here) --- src/Lean/MetavarContext.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 98e84d86c87b..ba51a21d1386 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -620,6 +620,21 @@ def instantiateMVarsCore (mctx : MetavarContext) (e : Expr) : Expr × MetavarCon instantiateExprMVars e runST fun _ => instantiate e |>.run |>.run mctx +/- +Substitutes assigned metavariables in `e` with their assigned value according to the +`MetavarContext`, recursively. + +Example: +``` +run_meta do + let mvar1 ← mkFreshExprMVar (mkConst `Nat) + let e := (mkConst `Nat.succ).app mvar1 + logInfo e -- Nat.succ ?m.773 + mvar1.mvarId!.assign (mkNatLit 42) + let e' ← instantiateMVars e + logInfo e' -- Nat.succ 42 +``` +-/ def instantiateMVars [Monad m] [MonadMCtx m] (e : Expr) : m Expr := do if !e.hasMVar then return e From c4a715d57c60db18678d50f223e86bc41c610f6c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 13 Apr 2024 09:55:00 +0200 Subject: [PATCH 2/3] Update src/Lean/MetavarContext.lean --- src/Lean/MetavarContext.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index ba51a21d1386..39e5ea5974b7 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -632,7 +632,11 @@ run_meta do logInfo e -- Nat.succ ?m.773 mvar1.mvarId!.assign (mkNatLit 42) let e' ← instantiateMVars e - logInfo e' -- Nat.succ 42 + -- e is `Nat.succ ?m.773`, `?m.773` is unassigned + mvar1.mvarId!.assign (mkNatLit 42) + -- e is `Nat.succ ?m.773`, `?m.773` is assigned to `42` + let e' ← instantiateMVars e + -- e' is `Nat.succ 42`, `?m.773` is assigned to `42` ``` -/ def instantiateMVars [Monad m] [MonadMCtx m] (e : Expr) : m Expr := do From 230ae8b1f5607a85a72fe5bdd662aefa7b105d2e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 15 Apr 2024 15:10:17 +0200 Subject: [PATCH 3/3] Update src/Lean/MetavarContext.lean --- src/Lean/MetavarContext.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 39e5ea5974b7..ec69b21b802d 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -629,9 +629,6 @@ Example: run_meta do let mvar1 ← mkFreshExprMVar (mkConst `Nat) let e := (mkConst `Nat.succ).app mvar1 - logInfo e -- Nat.succ ?m.773 - mvar1.mvarId!.assign (mkNatLit 42) - let e' ← instantiateMVars e -- e is `Nat.succ ?m.773`, `?m.773` is unassigned mvar1.mvarId!.assign (mkNatLit 42) -- e is `Nat.succ ?m.773`, `?m.773` is assigned to `42`