From 9515bbad5b58ed1c51ac6d9fc9d7a4e5884b6273 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jul 2023 15:23:53 +0200
Subject: Reorganize a bit the lean backend files

---
 backends/lean/Base/Diverge/Elab.lean | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'backends/lean/Base/Diverge')

diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index e5b39440..96f7abc0 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -2,6 +2,7 @@ import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
 import Mathlib.Tactic.RunCmd
+import Base.Utils
 import Base.Diverge.Base
 import Base.Diverge.ElabBase
 
@@ -13,6 +14,7 @@ namespace Diverge
 syntax (name := divergentDef)
   declModifiers "divergent" "def" declId ppIndent(optDeclSig) declVal : command
 
+open Utils
 open Lean Elab Term Meta Primitives Lean.Meta
 
 /- The following was copied from the `wfRecursion` function. -/
-- 
cgit v1.2.3