From 5adb04b10e4996a939a9976472df1b2ef15ec005 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Oct 2020 11:24:35 -0700
Subject: [PATCH] chore: add helper instance

---
 src/Init/Control/Id.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean
index 322231ff65..ddcd04417d 100644
--- a/src/Init/Control/Id.lean
+++ b/src/Init/Control/Id.lean
@@ -33,6 +33,9 @@ instance : Monad Id :=
 @[inline] protected def run {α : Type u} (x : Id α) : α :=
 x
 
+instance {α} [HasOfNat α] : HasOfNat (Id α) :=
+inferInstanceAs (HasOfNat α)
+
 instance : MonadRun id Id :=
 ⟨@Id.run⟩