back compatible with v4.13.0

Author: slashbade

REPL/Future.lean

@@ -0,0 +1,11 @@
+import Lean
+
+namespace List
+
+def flatten : List (List α) → List α
+  | []      => []
+  | a :: as => a ++ flatten as
+
+def flatMap {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β := flatten (map b a)
+
+end List

REPL/JSON.lean

@@ -6,9 +6,12 @@ Authors: Scott Morrison
 import Lean.Data.Json
 import Lean.Message
 import Lean.Elab.InfoTree.Main
+import REPL.Future
+
 
 open Lean Elab InfoTree
 
+
 namespace REPL
 
 structure CommandOptions where

REPL/Lean/InfoTree.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean
-
+import REPL.Future
 /-!
 Additional functions to deal with `InfoTree`.
 -/
@@ -214,13 +214,13 @@ def sorries (t : InfoTree) : List (ContextInfo × SorryType × Position × Posit
 
 def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × Position × Position × Array Name) :=
     -- HACK: creating a child ngen
-  t.findTacticNodes.map fun ⟨i, ctx⟩ => 
-    let range := stxRange ctx.fileMap i.stx 
-    ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 }, 
-      i.stx, 
-      i.goalsBefore, 
-      range.fst, 
-      range.snd, 
+  t.findTacticNodes.map fun ⟨i, ctx⟩ =>
+    let range := stxRange ctx.fileMap i.stx
+    ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 },
+      i.stx,
+      i.goalsBefore,
+      range.fst,
+      range.snd,
       i.getUsedConstantsAsSet.toArray )
 
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc1
+leanprover/lean4:v4.13.0