From c25b910edfdb84d0da13976a5f39c43a0472212c Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 26 Feb 2023 10:58:22 +0100
Subject: [PATCH] fix Main.idr

---
 exe/Main.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/exe/Main.idr b/exe/Main.idr
index 1470184..e92cb90 100644
--- a/exe/Main.idr
+++ b/exe/Main.idr
@@ -56,7 +56,7 @@ banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
 export
 tm : Term Three 1 2
 tm =
-  (Pi One "a" (BVT 0) (TUsed $ E (F "F" :@@ [BVT 0, FT "w"]))
+  (Pi_ One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
     `DCloT` (K One ::: id))
     `CloT`  (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)