An experimental type theory with scoped equality reflection, and non-arbitrary proof search. This is basically a pared down version of Andromeda/Brazil, but with untyped reduction and a more Nuprl-like feel. Computational content of proofs is got via a realizability-based extraction. (Note: substitution is unsafe here, not because of a problem w…
Haskell TeX
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
src
twelf
.gitignore Add some twelf noodlings Jun 29, 2014
.travis.yml
README.md
Setup.hs Beautify Jun 10, 2014
TT.cabal
cabal.config
rules.pdf Syntax, inference & computation for negative sigma eliminators Jul 4, 2014
rules.tex
stylish.defaults Beautify Jun 10, 2014
test.tt Remove separate identity intros; just use one constructor Jul 5, 2014

README.md

TT-Reflection

Requirements

  1. GHC 7.8.2
  2. cabal-install 1.20.0.x

See the learnhaskell for details on installing these.

This may work with previous versions of GHC and cabal, but I have zero interest in making sure that it does.

Building

$ cabal sandbox init
$ cabal install --only-dependencies
$ cabal configure
$ cabal build

Running

$ cabal run -- check test.tt    # check a theory file
$ cabal run -- repl             # start the REPL