name: Sit version: 0.2017.2.26 x-revision: 1 -- x-revision:1 see https://github.com/haskell-infra/hackage-trustees/issues/128 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, base >= 4.2 && < 5, containers >= 0.3 && < 1, data-lens-light >= 0.1.2.2 && < 0.2, mtl >= 2.2.1 && < 3 -- -- 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