From 9b12bd4e3c1c56debe2b673e66fff650dc608689 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Thu, 27 Jun 2024 16:27:56 +0300
Subject: [PATCH] [ elab, minor ] Implement `Functor` for `PiInfo`

---
 libs/base/Language/Reflection/TT.idr | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/libs/base/Language/Reflection/TT.idr b/libs/base/Language/Reflection/TT.idr
index 60b685ab59e..3344c553013 100644
--- a/libs/base/Language/Reflection/TT.idr
+++ b/libs/base/Language/Reflection/TT.idr
@@ -229,6 +229,13 @@ public export
 data PiInfo t = ImplicitArg | ExplicitArg | AutoImplicit | DefImplicit t
 %name PiInfo pinfo
 
+public export
+Functor PiInfo where
+  map f ImplicitArg     = ImplicitArg
+  map f ExplicitArg     = ExplicitArg
+  map f AutoImplicit    = AutoImplicit
+  map f $ DefImplicit x = DefImplicit $ f x
+
 export
 showPiInfo : Show a => {default True wrapExplicit : Bool} -> PiInfo a -> String -> String
 showPiInfo ImplicitArg s = "{\{s}}"