From 4fd17e4bb91eb46d4704643dfbfbbf0874837b07 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 4 Jul 2023 12:49:37 +0200
Subject: Make Diverge use Primitives

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

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

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))) :=
-- 
cgit v1.2.3