Additional utilities in Lean.MVarId
#
Applies intro
repeatedly until it fails. We use this instead of
Lean.MVarId.intros
to allowing unfolding.
For example, if we want to do introductions for propositions like ¬p
,
the ¬
needs to be unfolded into → False
, and intros
does not do such unfolding.
Equations
Instances For
Get the type the given metavariable after instantiating metavariables and cleaning up annotations.