From 2fa3cb8ee04dd7ff4184e3e1000fdc025abc50a4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jul 2023 23:37:48 +0200
Subject: Start proving theorems for primitive definitions

---
 backends/lean/Base/Diverge/Base.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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

diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 0a9ea4c4..4ff1d923 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -3,8 +3,7 @@ import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
 import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
-
-import Base.Primitives
+import Base.Primitives.Base
 
 /- TODO: this is very useful, but is there more? -/
 set_option profiler true
-- 
cgit v1.2.3