From 63417ef179066bfd847ff5efc5e74085268b1795 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 5 May 2024 00:43:32 -0700 Subject: [PATCH] fix: Motive extra arguments not instiantiated --- Pantograph/Tactic/MotivatedApply.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index 821b681..a7b9a07 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -32,8 +32,8 @@ protected def getMotiveType (info: RecursorWithMotive): Expr := let a := info.args.get! level a -protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr): MetaM Expr := do - let motiveType := info.getMotiveType +protected def surrogateMotiveType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do + let motiveType := Expr.instantiateRev info.getMotiveType mvars let resultantType ← Meta.inferType resultant return replaceForallBody motiveType resultantType @@ -83,7 +83,7 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do let argType := argType.instantiateRev prev let bvarIndex := info.nArgs - i - 1 let argGoal ← if bvarIndex = info.iMotive then - let surrogateMotiveType ← info.surrogateMotiveType resultant + let surrogateMotiveType ← info.surrogateMotiveType prev resultant Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) else Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)