From a3a7020df35df764e01802089bba21079dcb0ddd Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 31 Mar 2023 17:52:34 +0100
Subject: Add default names for the View types.

---
 src/Core/Thinning.idr | 2 ++
 src/Core/Var.idr      | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'src')

diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr
index 5781eaa..de0d5dc 100644
--- a/src/Core/Thinning.idr
+++ b/src/Core/Thinning.idr
@@ -49,6 +49,8 @@ data View : sx `Thins` sy -> Type where
     (0 prf : IsNotId thin) -> -- For uniqueness
     View (keep thin n)
 
+%name View view
+
 export
 view : (thin : sx `Thins` sy) -> View thin
 view IsId = Id sx
diff --git a/src/Core/Var.idr b/src/Core/Var.idr
index 502a416..25648e5 100644
--- a/src/Core/Var.idr
+++ b/src/Core/Var.idr
@@ -35,6 +35,8 @@ namespace View
     Here : View Core.Var.here
     There : (i : Var sx) -> View (there i)
 
+  %name View.View view
+
 export
 view : (i : Var sx) -> View i
 view (MakeVar 0 Here) = Here
-- 
cgit v1.2.3