Sit-0.2017.2.26: Sit.cabal
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