name: Sit version: 0.2017.02.26 build-type: Simple cabal-version: >= 1.8 license: OtherLicense license-file: LICENSE author: Anonymous maintainer: Anonymous homepage: NONE category: Dependent types synopsis: Prototypical type checker for Type Theory with Sized Natural Numbers description: 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 tested-with: GHC == 7.8.4 GHC == 7.10.3 GHC == 8.0.1 data-files: test/Makefile test/Base.agda test/Test.agda README.md extra-source-files: Makefile src/Makefile src/Sit.cf src/undefined.h source-repository head type: git location: NONE executable Sit.bin ghc-options: -rtsopts hs-source-dirs: src build-depends: array >= 0.3 && < 1.0, base >= 4.2 && < 5.0, containers >= 0.3 && < 1.0, data-lens-light >= 0.1.2.2 && < 0.2, mtl >= 2.2.1 && < 3.0 -- -- The lexer and parser are shipped as .hs files, thus, no tools necessary. -- build-tools: happy >= 1.15 && < 2, -- alex >= 3.0 && < 4 extensions: MultiParamTypeClasses FunctionalDependencies TypeSynonymInstances FlexibleInstances FlexibleContexts GeneralizedNewtypeDeriving LambdaCase TupleSections main-is: Sit.hs other-modules: Abstract Evaluation Impossible Internal Lens Substitute TypeChecker Sit.Abs Sit.ErrM Sit.Lex Sit.Par Sit.Print