MiniAgda-0.2016.12.19: MiniAgda.cabal
name: MiniAgda
version: 0.2016.12.19
build-type: Simple
cabal-version: >= 1.22
license: OtherLicense
license-file: LICENSE
author: Andreas Abel and Karl Mehltretter
maintainer: Andreas Abel <andreas.abel@ifi.lmu.de>
homepage: http://www.tcs.ifi.lmu.de/~abel/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.1
extra-source-files: Makefile
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.17 && < 1.18,
mtl >= 2.2.0.1 && < 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
Main
Parser
Polarity
PrettyTCM
ScopeChecker
Semiring
SparseMatrix
TCM
Termination
ToHaskell
Tokens
TraceError
TreeShapedOrder
TypeChecker
Util
Value
Warshall