-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Prototypical type checker for Type Theory with Sized Natural Numbers
--   
--   Sit = Size-irrelevant types
--   
--   Sit is a prototypical language with an Agda-compatible syntax. It has
--   dependent function types, universes, sized natural numbers, and case
--   and recursion over natural numbers. There is a relevant and an
--   irrelevant quantifier over sizes. For an example, see file
--   test/Test.agda.
@package Sit
@version 0.2022.3.18

module Sit

-- | Type-check file given by command line.
main :: IO ()

-- | Run the type checker on text/contents of a file.
check :: String -> IO ()

-- | Run the type checker on file given by path.
checkFile :: FilePath -> IO ()