name: MiniAgda version: 0.2018.11.4 build-type: Simple cabal-version: 1.24 license: OtherLicense license-file: LICENSE author: Andreas Abel and Karl Mehltretter maintainer: Andreas Abel homepage: http://www.cse.chalmers.se/~abela/miniagda/ bug-reports: https://github.com/andreasabel/miniagda/issues category: Dependent types synopsis: A toy dependently typed programming language with type-based termination. description: MiniAgda is a tiny dependently-typed programming language in the style of Agda. It serves as a laboratory to test potential additions to the language and type system of Agda. MiniAgda's termination checker is a fusion of sized types and size-change termination and supports coinduction. Equality incorporates eta-expansion at record and singleton types. Function arguments can be declared as static; such arguments are discarded during equality checking and compilation. Recent features include bounded size quantification and destructor patterns for a more general handling of coinduction. tested-with: GHC == 7.6.3 GHC == 7.8.4 GHC == 7.10.3 GHC == 8.0.2 GHC == 8.2.2 GHC == 8.4.4 extra-source-files: Makefile CHANGELOG README.md data-files: test/succeed/Makefile test/succeed/*.ma test/fail/Makefile test/fail/*.ma test/fail/*.err test/fail/adm/*.ma test/fail/adm/*.err lib/*.ma source-repository head type: git location: https://github.com/andreasabel/miniagda executable miniagda hs-source-dirs: src build-depends: array >= 0.3 && < 0.6, base >= 4.6 && < 5, containers >= 0.3 && < 0.6, haskell-src-exts >= 1.20 && < 2.0, mtl >= 2.2.2 && < 2.3, pretty >= 1.0 && < 1.2 build-tools: happy >= 1.15 && < 2, alex >= 3.0 && < 4 default-language: Haskell98 default-extensions: CPP MultiParamTypeClasses TypeSynonymInstances FlexibleInstances FlexibleContexts GeneralizedNewtypeDeriving NoMonomorphismRestriction PatternGuards TupleSections NamedFieldPuns main-is: Main.hs other-modules: Abstract Collection Concrete Eval Extract HsSyntax Lexer Parser Polarity PrettyTCM ScopeChecker Semiring SparseMatrix TCM Termination ToHaskell Tokens TraceError TreeShapedOrder TypeChecker Util Value Warshall