Use Lean with built-in RPINF

leanprover-community · Feb 8, 2025 · 0425705 · 0425705
1 parent 83b5a66
commit 0425705
Show file tree

Hide file tree

Showing 5 changed files with 3 additions and 149 deletions.
diff --git a/Aesop/BaseM.lean b/Aesop/BaseM.lean
@@ -9,7 +9,7 @@ import Aesop.RulePattern.Cache
 
 set_option linter.missingDocs true
 
-open Lean
+open Lean Lean.Meta
 
 namespace Aesop
 

diff --git a/Aesop/Forward/Substitution.lean b/Aesop/Forward/Substitution.lean
@@ -6,7 +6,6 @@ Authors: Jannis Limperg
 
 import Aesop.Forward.LevelIndex
 import Aesop.Forward.PremiseIndex
-import Aesop.RPINF.Basic
 import Aesop.Util.Basic
 
 namespace Aesop

diff --git a/Aesop/RPINF/Basic.lean b/Aesop/RPINF/Basic.lean
diff --git a/Aesop/RulePattern.lean b/Aesop/RulePattern.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
+import Aesop.BaseM
 import Aesop.Forward.Substitution
-import Aesop.RPINF
 import Aesop.Rule.Name
 import Aesop.Tracing
 import Aesop.Index.DiscrTreeConfig

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.17.0-rc1
+lean4-work