name: Sit version: 0.2021.1.18 build-type: Simple cabal-version: >= 1.10 license: OtherLicense license-file: LICENSE author: Andreas Abel maintainer: Andreas Abel homepage: https://github.com/andreasabel/Sit 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.2 GHC == 8.2.2 GHC == 8.4.4 GHC == 8.6.5 GHC == 8.8.4 GHC == 8.10.3 data-files: test/Makefile test/Base.agda test/Test.agda extra-source-files: Makefile src/Makefile src/Sit.cf src/undefined.h CHANGELOG.md README.md source-repository head type: git location: https://github.com/andreasabel/Sit library 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 default-language: Haskell98 other-extensions: MultiParamTypeClasses FunctionalDependencies TypeSynonymInstances FlexibleInstances FlexibleContexts GeneralizedNewtypeDeriving LambdaCase TupleSections exposed-modules: Sit other-modules: Abstract Evaluation Impossible Internal Lens Substitute TypeChecker Sit.Abs Sit.Lex Sit.Par Sit.Print executable Sit.bin hs-source-dirs: main main-is: Main.hs build-depends: base, Sit default-language: Haskell98 ghc-options: -rtsopts test-suite system-test type: exitcode-stdio-1.0 hs-source-dirs: test main-is: Main.hs other-modules: Paths_Sit build-depends: base, Sit default-language: Haskell98