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) (TUsed $ 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