name: helf version: 0.2021.8.12 build-type: Simple cabal-version: >= 1.10 license: MIT license-file: LICENSE author: Andreas Abel and Nicolai Kraus maintainer: Andreas Abel homepage: http://www2.tcs.ifi.lmu.de/~abel/projects.html#helf category: Dependent types synopsis: Typechecking terms of the Edinburgh Logical Framework (LF). description: HELF = Haskell implementation of the Edinburgh Logical Framework . HELF implements only a subset of the Twelf syntax and functionality. It type-checks LF definitions, but does not do type reconstruction. 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 GHC == 8.6.5 GHC == 8.8.4 GHC == 8.10.4 GHC == 9.0.1 data-files: test/succeed/Makefile test/succeed/*.elf test/fail/Makefile test/fail/*.elf test/fail/*.err extra-source-files: Makefile src/Makefile README.md CHANGELOG.md source-repository head type: git location: https://github.com/andreasabel/helf executable helf ghc-options: -rtsopts hs-source-dirs: src build-depends: array >= 0.3 && < 1.0, base >= 4.2 && < 5.0, containers >= 0.3 && < 1.0, mtl >= 2.2.1 && < 3.0, pretty >= 1.0 && < 2.0, QuickCheck >= 2.4 && < 3.0 build-tools: happy >= 1.15 && < 2, alex >= 3.0 && < 4 default-language: Haskell2010 default-extensions: MultiParamTypeClasses FunctionalDependencies UndecidableInstances OverlappingInstances TypeSynonymInstances FlexibleInstances FlexibleContexts GeneralizedNewtypeDeriving TupleSections main-is: Main.hs other-modules: Abstract ClosVal Closures Concrete Context DataStructure DatastrucImpl.List DatastrucImpl.StrictDynArray Fresh HerBruijn HerBruijnVal Lexer ListEnv LocallyNamelessSyntax MapEnv MonoVal Monolith NamedExplSubst ORef OperatorPrecedenceParser OrderedCom2 OrderedComplex2 Parser PrettyM ScopeMonad Scoping Signature TGChecker TermGraph TheMonad TypeCheck Util Value