From 2c08ef1e23a3429cefb5aacad19819a92768a847 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 2 Aug 2024 19:53:19 -0700 Subject: [PATCH] refactor: Remove old `visibleFVars` interface --- Pantograph/Goal.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index ccb7a3d..26a8da1 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -69,15 +69,6 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O protected def GoalState.metaState (state: GoalState): Meta.State := state.savedState.term.meta.meta --- Get the list of visible free variables from a goal -@[export pantograph_goal_state_visible_fvars] -protected def GoalState.visibleFVars (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do - let mvarDecl ← state.mctx.findDecl? mvarId - let lctx := mvarDecl.lctx - return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with - | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId - | none => r - protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState