From 72d35d4ce84a863bb4d96b844fb552028d94234a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 15 May 2023 13:08:49 +0200
Subject: Add Result_Inhabited to Primitives.lean

---
 tests/lean/misc-no_nested_borrows/Base/Primitives.lean | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'tests/lean/misc-no_nested_borrows/Base')

diff --git a/tests/lean/misc-no_nested_borrows/Base/Primitives.lean b/tests/lean/misc-no_nested_borrows/Base/Primitives.lean
index 034f41b2..4a66a453 100644
--- a/tests/lean/misc-no_nested_borrows/Base/Primitives.lean
+++ b/tests/lean/misc-no_nested_borrows/Base/Primitives.lean
@@ -49,6 +49,9 @@ deriving Repr, BEq
 
 open Result
 
+instance Result_Inhabited (α : Type u) : Inhabited (Result α) :=
+  Inhabited.mk (fail panic)
+
 /- HELPERS -/
 
 def ret? {α: Type} (r: Result α): Bool :=
-- 
cgit v1.2.3