summaryrefslogtreecommitdiff
path: root/src/Core/Var.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Core/Var.idr')
-rw-r--r--src/Core/Var.idr2
1 files changed, 2 insertions, 0 deletions
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