2021-07-07 07:11:39 -04:00
|
|
|
module Quox
|
|
|
|
|
2021-09-09 17:51:00 -04:00
|
|
|
import public Quox.Syntax
|
2021-07-20 16:05:19 -04:00
|
|
|
import public Quox.Pretty
|
|
|
|
|
|
|
|
import Data.Nat
|
|
|
|
import Data.Vect
|
|
|
|
|
|
|
|
|
|
|
|
export
|
|
|
|
tm : Term 1 2
|
|
|
|
tm =
|
|
|
|
(Pi Zero One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
|
|
|
|
`DCloT` (DOne ::: id))
|
|
|
|
`CloT` (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)
|
|
|
|
|
2021-07-07 07:11:39 -04:00
|
|
|
main : IO Unit
|
2021-07-20 16:05:19 -04:00
|
|
|
main = do
|
|
|
|
prettyTerm tm
|
|
|
|
prettyTerm $ pushSubstsT tm
|
|
|
|
putStrLn ":qtuwu:"
|