aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

refactor: Un-export two field accessor functions 

User should use `lean_ctor_get`
This commit is contained in:
Leni Aniva 2024-09-08 11:53:10 -07:00
parent 4042ec707e
commit 7c49fcff27
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 0 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Pantograph/Goal.lean
View File

@ -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.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
protected def GoalState.mctx (state: GoalState): MetavarContext := protected def GoalState.mctx (state: GoalState): MetavarContext :=
state.savedState.term.meta.meta.mctx state.savedState.term.meta.meta.mctx
@[export pantograph_goal_state_env]
protected def GoalState.env (state: GoalState): Environment := protected def GoalState.env (state: GoalState): Environment :=
state.savedState.term.meta.core.env 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 protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
let mvarDecl ← state.mctx.findDecl? mvarId let mvarDecl ← state.mctx.findDecl? mvarId
return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances } return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
@[export pantograph_goal_state_meta_state]
protected def GoalState.metaState (state: GoalState): Meta.State := protected def GoalState.metaState (state: GoalState): Meta.State :=
state.savedState.term.meta.meta state.savedState.term.meta.meta