3 files changed, 6 insertions, 69 deletions
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index a8503107..e22eb914 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -4,8 +4,7 @@ import Init.Data.List.Basic
 import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 
--- For debugging
-import Base.Diverge.ElabBase
+import Base.Primitives
 
 /-
 TODO:
@@ -35,68 +34,6 @@ set_option profiler.threshold 100
 
 namespace Diverge
 
-namespace Primitives
-/-! # Copy-pasting from Primitives to make the file self-contained -/
-
-inductive Error where
-   | assertionFailure: Error
-   | integerOverflow: Error
-   | divisionByZero: Error
-   | arrayOutOfBounds: Error
-   | maximumSizeExceeded: Error
-   | panic: Error
-deriving Repr, BEq
-
-open Error
-
-inductive Result (α : Type u) where
-  | ret (v: α): Result α
-  | fail (e: Error): Result α
-  | div
-deriving Repr, BEq
-
-open Result
-
-instance Result_Inhabited (α : Type u) : Inhabited (Result α) :=
-  Inhabited.mk (fail panic)
-
-instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
-  Nonempty.intro div
-
-def bind {α : Type u} {β : Type v} (x: Result α) (f: α -> Result β) : Result β :=
-  match x with
-  | ret v  => f v 
-  | fail v => fail v
-  | div => div
-
-@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind]
-@[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind]
-@[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind]
-
--- Allows using Result in do-blocks
-instance : Bind Result where
-  bind := bind
-
--- Allows using return x in do-blocks
-instance : Pure Result where
-  pure := fun x => ret x
-
-@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) :
-  (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind]
-
-@[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) :
-  (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind]
-
-@[simp] theorem bind_tc_div (f : α → Result β) :
-  (do let y ← div; f y) = div := by simp [Bind.bind, bind]
-
-def div? {α: Type u} (r: Result α): Bool :=
-  match r with
-  | div => true
-  | ret _ | fail _ => false
-
-end Primitives
-
 namespace Fix
 
   open Primitives
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index cc580265..41209021 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -174,7 +174,7 @@ private def list_nth_out_ty_inner (a :Type) (scrut1: @Sigma (List a) (fun (_ls :
                  (fun (_ls : List a) => Int)
                  (fun (_scrut1:@Sigma (List a) (fun (_ls : List a) => Int)) => Type)
                  scrut1
-                 (fun (_ls : List a) (_i : Int) => Diverge.Primitives.Result a)
+                 (fun (_ls : List a) (_i : Int) => Primitives.Result a)
 
 private def list_nth_out_ty_outer (scrut0 : @Sigma (Type) (fun (a:Type) =>
                       @Sigma (List a) (fun (_ls : List a) => Int))) :=
diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean
index fd95291e..1c1062c0 100644
--- a/backends/lean/Base/Diverge/ElabBase.lean
+++ b/backends/lean/Base/Diverge/ElabBase.lean
@@ -4,6 +4,7 @@ namespace Diverge
 
 open Lean Elab Term Meta
 
+-- We can't define and use trace classes in the same file
 initialize registerTraceClass `Diverge.elab
 initialize registerTraceClass `Diverge.def
 initialize registerTraceClass `Diverge.def.sigmas
@@ -11,8 +12,8 @@ initialize registerTraceClass `Diverge.def.genBody
 initialize registerTraceClass `Diverge.def.valid
 initialize registerTraceClass `Diverge.def.unfold
 
--- TODO: move
--- TODO: small helper
+-- Useful helper to explore definitions and figure out the variant
+-- of their sub-expressions.
 def explore_term (incr : String) (e : Expr) : MetaM Unit :=
   match e with
   | .bvar _ => do logInfo m!"{incr}bvar: {e}"; return ()
@@ -81,8 +82,7 @@ private def test2 (x : Nat) : Nat := x
 print_decl test1
 print_decl test2
 
--- We adapted this from AbstractNestedProofs.visit
--- A map visitor function for expressions
+-- A map visitor function for expressions (adapted from `AbstractNestedProofs.visit`)
 partial def mapVisit (k : Expr → MetaM Expr) (e : Expr) : MetaM Expr := do
   let mapVisitBinders (xs : Array Expr) (k2 : MetaM Expr) : MetaM Expr := do
     let localInstances ← getLocalInstances