From 0c30372f93199f7e021f5773c8fd824af2b3668c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Jul 2022 20:08:12 -0700 Subject: [PATCH] doc: add todo for `expandDelayedAssigned` --- src/Lean/Meta/ExprDefEq.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 6880db6d68..bdd1ea281b 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -1279,7 +1279,16 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do That is, `instantiateMVars (mkMVar mvarIdPending)` does not contain any expression metavariables. Here we just consume `fvar.size` arguments. That is, if `t` is of the form `mvarId as bs` where `as.size == fvars.size`, we return `mvarIdPending bs`. - -/ + + TODO: improve this transformation. Here is a possible improvement. + Assume `t` is of the form `?m as` where `as` represent the arguments, and we are trying to solve + `?m as =?= s[as]` where `s[as]` represents a term containing occurrences of `as`. + We could try to compute the solution as usual `?m := fun ys => s[as/ys]` + We also have the delayed assignment `?m [xs] := ?n`, where `xs` are variables in the scope of `?n`, + and this delayed assignment is morally `?m := fun xs => ?n`. + Thus, we can reduce `?m as =?= s[as]` to `?n =?= s[as/xs]`, and solve it using `?n`'s local context. + This is more precise than simplying droping the arguments `as`. + -/ unless (← getConfig).assignSyntheticOpaque do return none let tArgs := t.getAppArgs if tArgs.size < fvars.size then return none