From aa106f7591b8719ce91baa25e7434b808b62e0d6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 6 May 2024 22:20:20 -0700 Subject: [PATCH] feat: Do not filter mvars from mapply --- Pantograph/Tactic/MotivatedApply.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index a7b9a07..f570560 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -94,11 +94,11 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do -- Create the conduit type which proves the result of the motive is equal to the goal let conduitType ← info.conduitType newMVars resultant - let goalConduit ← Meta.mkFreshExprMVar conduitType .syntheticOpaque (userName := `conduit) + let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit) goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars) newMVars := newMVars ++ [goalConduit] - let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned) + let nextGoals := newMVars.toList.map (·.mvarId!) pure nextGoals Elab.Tactic.setGoals nextGoals