homepage: http://www2.tcs.ifi.lmu.de/~abel/projects.html#helf
changelog-type: ''
hash: e10b725b12025f3926de6a22679eaed779d9224eeced081125d70fea834ef541
test-bench-deps: {}
maintainer: Andreas Abel <andreas.abel@ifi.lmu.de>
synopsis: Typechecking terms of the Edinburgh Logical Framework (LF).
changelog: ''
basic-deps:
  base: ! '>=4.2 && <5.0'
  array: ! '>=0.3 && <1.0'
  containers: ! '>=0.3 && <1.0'
  mtl: ! '>=2.2.1 && <3.0'
  QuickCheck: ! '>=2.4 && <3.0'
  pretty: ! '>=1.0 && <2.0'
all-versions:
- '0.2016.12.25'
author: Andreas Abel and Nicolai Kraus
latest: '0.2016.12.25'
description-type: markdown
description: ! "# helf\nA Haskell implementation of the Edinburgh Logical Framework.\n\nhelf
  parses and typechecks `.elf` files written for the Twelf implementation\nof the
  Logical Framework.  helf is mainly a laboratory to experiment with different\nrepresentation
  of lambda-terms for bidirectional typechecking.\n\n## Limitations\n\nhelf only understands
  a subset of the Twelf language and implements only a small subset of Twelf's features.\n+
  helf does not parse the backarrow `<-` notation for function space.\n+ helf only
  understands the fixity pragmas for operators.  It ignores all other pragmas.\n+
  helf only implements bidirectional type checking.  It does not have unification
  or type reconstruction.\n+ helf does not give nice error messages.\n\n## Installation\n\nRequires
  GHC and cabal, for instance via the Haskell Platform.\nIn a shell, type\n```\n  cabal
  install helf\n```\n\n## Examples\n\nFile `eval.elf`:\n```elf\n% Untyped lambda calculus.\n\ntm
  \  : type.\nabs  : (tm -> tm) -> tm.\napp  : tm -> (tm -> tm).\n\n% cbn weak head
  evaluation.\n\neval : tm -> tm -> type.\n\neval/abs : {M : tm -> tm}\n  eval (abs
  M) (abs M).\n\neval/app : {M : tm} {M' : tm -> tm} {N : tm} {V : tm}\n  eval M (abs
  M') ->\n  eval (M' N) V   ->\n  eval (app M N) V.\n```\nType check with:\n```\n
  \ helf eval.elf\n```\n\nFor more examples, see `test/succeed/`.\n"
license-name: OtherLicense

Update from Hackage at 2016-12-25T20:56:15Z
Update from Hackage at 2016-12-25T20:56:15Z
