def Lean.MVarId.isIndependentOf (L : List MVarId) (g : MVarId) : MetaM Bool

Check if a goal is "independent" of a list of other goals. We say a goal is independent of other goals if assigning a value to it can not change the assignability of the other goals.

Examples:

• ?m_1 : Type is not independent of ?m_2 : ?m_1, because we could assign true : Bool to ?m_2, but if we first assign Nat to ?m_1 then that is no longer possible.
• ?m_1 : Nat is not independent of ?m_2 : Fin ?m_1, because we could assign 37 : Fin 42 to ?m_2, but if we first assign 2 to ?m_1 then that is no longer possible.
• ?m_1 : ?m_2 is not independent of ?m_2 : Type, because we could assign Bool to ?m_2, but if we first assign 0 : Natto?m_1` then that is no longer possible.
• Given P : Prop and f : P → Type, ?m_1 : P is independent of ?m_2 : f ?m_1 by proof irrelevance.
• Similarly given f : Fin 0 → Type, ?m_1 : Fin 0 is independent of ?m_2 : f ?m_1, because Fin 0 is a subsingleton.
• Finally ?m_1 : Nat is independent of ?m_2 : α, as long as ?m_1 does not appear in Meta.getMVars α (note that Meta.getMVars follows delayed assignments).

This function only calculates a conservative approximation of this condition. That is, it may return false when it should return true. (In particular it returns false whenever the type of g contains a metavariable, regardless of whether this is related to the metavariables in L.)

Equations

• One or more equations did not get rendered due to their size.