From 7c49fcff2760e8df7dbdb1c9189a3a8c4ac872c3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Sep 2024 11:53:10 -0700 Subject: [PATCH] refactor: Un-export two field accessor functions User should use `lean_ctor_get` --- Pantograph/Goal.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 0109204..beba847 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -56,7 +56,6 @@ protected def GoalState.goals (state: GoalState): List MVarId := protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray protected def GoalState.mctx (state: GoalState): MetavarContext := state.savedState.term.meta.meta.mctx -@[export pantograph_goal_state_env] protected def GoalState.env (state: GoalState): Environment := state.savedState.term.meta.core.env @@ -64,7 +63,6 @@ protected def GoalState.env (state: GoalState): Environment := protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do let mvarDecl ← state.mctx.findDecl? mvarId return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances } -@[export pantograph_goal_state_meta_state] protected def GoalState.metaState (state: GoalState): Meta.State := state.savedState.term.meta.meta