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

chore: Code cleanup

This commit is contained in:
Leni Aniva 2025-05-02 11:26:17 -04:00
parent 120eb90291
commit 3bb8e75787
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 1 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Repl.lean
View File

@ -5,8 +5,6 @@ namespace Pantograph.Repl
open Lean open Lean
set_option trace.Pantograph.Frontend.MetaTranslate true
structure Context where structure Context where
coreContext : Core.Context coreContext : Core.Context
@ -30,7 +28,7 @@ instance : MonadEnv MainM where
getEnv := return (← get).env getEnv := return (← get).env
modifyEnv f := modify fun s => { s with env := f s.env } modifyEnv f := modify fun s => { s with env := f s.env }
def newGoalState (goalState: GoalState) : MainM Nat := do def newGoalState (goalState : GoalState) : MainM Nat := do
let state ← get let state ← get
let stateId := state.nextId let stateId := state.nextId
set { state with set { state with

4
Test/Tactic/Prograde.lean
View File

@ -131,10 +131,6 @@ def test_define_root_expr : TestT Elab.TermElabM Unit := do
let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr" let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n let binder := x.fst;\n binder 5") addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n let binder := x.fst;\n binder 5")
--set_option pp.all true
--#check @PSigma (α := Prop) (β := λ (p: Prop) => p)
--def test_define_root_expr : TestT Elab.TermElabM Unit := do
def test_have_proof : TestT Elab.TermElabM Unit := do def test_have_proof : TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))" let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
let state0 ← GoalState.create rootExpr let state0 ← GoalState.create rootExpr