[ elab, minor ] Implement Functor for PiInfo

buzden · Jun 27, 2024 · 9b12bd4 · 9b12bd4
1 parent f561c78
commit 9b12bd4
Showing 1 changed file with 7 additions and 0 deletions.
diff --git 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}}"