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

feat: Condensed interface #85

Merged
aniva merged 27 commits from serial/expr into dev 2024-08-15 22:41:59 -07:00
Conversation 0 Commits 27 Files Changed 13 -9
1 changed files with 0 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 2c08ef1e23 - Show all commits

9
Pantograph/Goal.lean
View File

@ -69,15 +69,6 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O
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
-- 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 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
mvarId.withContext m |>.run' (← read) state.metaState mvarId.withContext m |>.run' (← read) state.metaState