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

feat: Export GoalState.goalsArray

This commit is contained in:
Leni Aniva 2024-07-30 17:02:41 -07:00
parent 3ca52517ab
commit caa463f410
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 2 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Pantograph/Expr.lean
View File

@ -23,7 +23,6 @@ def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
inner, inner,
} }
def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/ /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/

2
Pantograph/Goal.lean
View File

@ -54,6 +54,8 @@ protected def GoalState.isConv (state: GoalState): Bool :=
state.convMVar?.isSome state.convMVar?.isSome
protected def GoalState.goals (state: GoalState): List MVarId := protected def GoalState.goals (state: GoalState): List MVarId :=
state.savedState.tactic.goals state.savedState.tactic.goals
@[export pantograph_goal_state_goals]
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
protected def GoalState.env (state: GoalState): Environment := protected def GoalState.env (state: GoalState): Environment :=

11
Pantograph/Library.lean
View File

@ -76,17 +76,6 @@ def createCoreState (imports: Array String): IO Core.State := do
(trustLevel := 1) (trustLevel := 1)
return { env := env } return { env := env }
@[export pantograph_env_catalog_m]
def envCatalog: CoreM Protocol.EnvCatalogResult :=
Environment.catalog ({}: Protocol.EnvCatalog)
@[export pantograph_env_inspect_m]
def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
CoreM (Protocol.CR Protocol.EnvInspectResult) :=
Environment.inspect ({
name, value? := .some value, dependency?:= .some dependency
}: Protocol.EnvInspect) options
@[export pantograph_env_add_m] @[export pantograph_env_add_m]
def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
CoreM (Protocol.CR Protocol.EnvAddResult) := CoreM (Protocol.CR Protocol.EnvAddResult) :=