max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: reduce import closure of MPL (#9382)

Browse source 
This PR reduces the import closure of the monadic verification framework
from `Lean.Meta` to only
the submodules actually required.
This commit is contained in:
Henrik Böving 2025-07-15 18:36:03 +02:00 • committed by GitHub
parent 6adeab2160
commit aa6f22d102
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Tactic/Do/Attr.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Graf
-/
prelude
import Lean.Meta
import Lean.Meta.Tactic.Simp
import Std.Do.Triple.Basic
import Std.Tactic.Do.Syntax

2
src/Lean/Elab/Tactic/Do/LetElim.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Graf
-/
prelude
import Lean.Meta
import Lean.Meta.Tactic.Simp
namespace Lean.Elab.Tactic.Do

2
src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean
View file

@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lars König, Mario Carneiro, Sebastian Graf
-/
prelude
import Lean.Meta
import Std.Tactic.Do.Syntax
import Lean.Meta.Basic
import Lean.Elab.Tactic.Do.ProofMode.MGoal
namespace Lean.Elab.Tactic.Do.ProofMode

1
src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean
View file

@ -5,6 +5,7 @@ Authors: Lars König, Mario Carneiro, Sebastian Graf
-/
prelude
import Lean.Elab.Tactic.Do.ProofMode.MGoal
import Lean.PrettyPrinter.Delaborator.Basic
namespace Lean.Elab.Tactic.Do.ProofMode
open Std.Do

1
src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean
View file

@ -7,6 +7,7 @@ prelude
import Std.Tactic.Do.Syntax
import Lean.Elab.Tactic.Do.ProofMode.Basic
import Lean.Elab.Tactic.Do.ProofMode.Focus
import Lean.Elab.Tactic.ElabTerm
namespace Lean.Elab.Tactic.Do.ProofMode
open Std.Do SPred.Tactic

1
src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean
View file

@ -5,7 +5,6 @@ Authors: Lars König, Mario Carneiro, Sebastian Graf
-/
prelude
import Lean.Elab.Tactic.Do.ProofMode.MGoal
import Lean.Meta
namespace Lean.Elab.Tactic.Do.ProofMode
open Std.Do SPred.Tactic ProofMode

4
src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean
View file

@ -6,7 +6,9 @@ Authors: Lars König, Mario Carneiro, Sebastian Graf
prelude
import Std.Do.SPred.DerivedLaws
import Std.Tactic.Do.ProofMode
import Lean.Meta
import Lean.SubExpr
import Lean.Meta.Basic
import Lean.Elab.Tactic.Basic
namespace Lean.Elab.Tactic.Do.ProofMode

1
src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean
View file

@ -9,6 +9,7 @@ import Lean.Elab.Tactic.Do.ProofMode.MGoal
import Lean.Elab.Tactic.Do.ProofMode.Focus
import Lean.Elab.Tactic.Do.ProofMode.Basic
import Lean.Elab.Tactic.Do.ProofMode.Pure
import Lean.Elab.Tactic.ElabTerm
namespace Lean.Elab.Tactic.Do.ProofMode
open Std.Do SPred.Tactic

1
src/Lean/Elab/Tactic/Do/VCGen.lean
View file

@ -7,6 +7,7 @@ prelude
import Init.Guard
import Std.Do.WP
import Std.Do.Triple
import Lean.Meta.Tactic.Split
import Lean.Elab.Tactic.Simp
import Lean.Elab.Tactic.Meta
import Lean.Elab.Tactic.Do.ProofMode.Basic