rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

fix Main.idr

Browse source
This commit is contained in:
rhiannon morris 2023-02-26 10:58:22 +01:00
parent 79a828449a
commit c25b910edf
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
exe/Main.idr
View file

@ -56,7 +56,7 @@ banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
export export
tm : Term Three 1 2 tm : Term Three 1 2
tm = 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)) `DCloT` (K One ::: id))
`CloT` (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id) `CloT` (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)