name: Sit version: 0.2023.8.3 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 == 9.6.2 GHC == 9.4.5 GHC == 9.2.8 GHC == 9.0.2 GHC == 8.10.7 GHC == 8.8.4 GHC == 8.6.5 GHC == 8.4.4 GHC == 8.2.2 GHC == 8.0.2 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.7 && < 5, containers >= 0.3 && < 1, data-lens-light >= 0.1.2.2 && < 0.2, mtl >= 2.2.1 && < 3 build-tools: alex >= 3.2.2 && < 4 , happy >= 1.19.6 && < 2 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