more logs

Author: GulinSS

src/TTImp/Elab/Check.idr

@@ -74,6 +74,14 @@ Show (ImplBinding vars) where
   show (NameBinding _ c p tm ty) = show (tm, ty)
   show (AsBinding c p tm ty pat) = show (tm, ty) ++ "@" ++ show tm
 
+export
+HasNames (ImplBinding vars) where
+  full gam (NameBinding fc c p tm ty) = pure (NameBinding fc c p !(full gam tm) !(full gam ty))
+  full gam (AsBinding c p tm ty pat) = pure (AsBinding c p tm !(full gam ty) !(full gam pat))
+
+  resolved gam (NameBinding fc c p tm ty) = pure (NameBinding fc c p !(resolved gam tm) !(resolved gam ty))
+  resolved gam (AsBinding c p tm ty pat) = pure (AsBinding c p tm !(resolved gam ty) !(resolved gam pat))
+
 export
 bindingMetas : ImplBinding vars -> NameMap Bool
 bindingMetas (NameBinding _ c p tm ty) = getMetas ty