38 lines
709 B
Idris
38 lines
709 B
Idris
module Quox
|
||
|
||
import public Quox.Name
|
||
import public Quox.Syntax
|
||
import public Quox.Equal
|
||
import public Quox.Error
|
||
import public Quox.Pretty
|
||
-- import public Quox.Typechecker
|
||
|
||
import Data.Nat
|
||
import Data.Vect
|
||
|
||
|
||
export
|
||
banner : String
|
||
banner = #"""
|
||
_ ___,-´/
|
||
(.`--´ ∪ -´/ ___ ___ _____ __ __
|
||
\/\/--´`´`--´ / _ `/ // / _ \\ \ /
|
||
U ---, / \_, /\_,_/\___/_\_\
|
||
/--/ | /_/
|
||
/--/ |
|
||
|
||
"""#
|
||
|
||
export
|
||
tm : Term 1 2
|
||
tm =
|
||
(Pi Zero 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)
|
||
|
||
main : IO Unit
|
||
main = do
|
||
putStrLn banner
|
||
prettyTerm tm
|
||
prettyTerm $ pushSubstsT tm
|