working on ZipN, with Garrin and Harley; also added support for evaluation of Pi-types, with Garrin; there is a bug where patterns in case-terms are not getting erased properly, which Garrin is going to tackle

git-svn-id: https://trellys.googlecode.com/svn/trunk@291 59285afe-504e-ee2a-6240-25eb0d263adb
cleaned up some code in TwoLevelTut.hs and clarified the questions



git-svn-id: https://trellys.googlecode.com/svn/trunk@292 59285afe-504e-ee2a-6240-25eb0d263adb
clarified the questions with the example


git-svn-id: https://trellys.googlecode.com/svn/trunk@293 59285afe-504e-ee2a-6240-25eb0d263adb
Error message cleanup.

git-svn-id: https://trellys.googlecode.com/svn/trunk@294 59285afe-504e-ee2a-6240-25eb0d263adb
Fixed erasure of patterns in case alternatives to drop compiletime pattern variables.

git-svn-id: https://trellys.googlecode.com/svn/trunk@295 59285afe-504e-ee2a-6240-25eb0d263adb
covering some missing cases for Abort, added a primitive show to print types of things while type-checking, and encountered what looks like a type-checker bug working on ZipN.

git-svn-id: https://trellys.googlecode.com/svn/trunk@296 59285afe-504e-ee2a-6240-25eb0d263adb
Added termination cast.

Demonstrated the use of the construct in Vectors append_assoc. That hurt.

git-svn-id: https://trellys.googlecode.com/svn/trunk@297 59285afe-504e-ee2a-6240-25eb0d263adb
Defined arity-generic zip. Didn't actually fix Aaron's problems with nested contexts.

The definition relies on a trusted termination proof (vector map terminates on terminating inputs).

Also included are a number of small bugfixes, error message cleanups, and morejoin enhancements.

git-svn-id: https://trellys.googlecode.com/svn/trunk@298 59285afe-504e-ee2a-6240-25eb0d263adb
working through examples from Thorsten and Conor's paper Generic Programming within Dependently Typed Programming; there is a type-checker bug, I think, which is blocking the last definition in the file

git-svn-id: https://trellys.googlecode.com/svn/trunk@299 59285afe-504e-ee2a-6240-25eb0d263adb
Fixed a problem in Aaron's example.

git-svn-id: https://trellys.googlecode.com/svn/trunk@300 59285afe-504e-ee2a-6240-25eb0d263adb
Added preliminary support for implicit (inferred) arguments.

Added some better syntax for declarations, eliminating some redundancy.

Check the module 'ImplicitArgs.sep' for some trivial examples of both.

git-svn-id: https://trellys.googlecode.com/svn/trunk@301 59285afe-504e-ee2a-6240-25eb0d263adb
Minor bug fix to get package to build with cabal.

git-svn-id: https://trellys.googlecode.com/svn/trunk@302 59285afe-504e-ee2a-6240-25eb0d263adb
Cleanup and reorg of matching for implicit args.

git-svn-id: https://trellys.googlecode.com/svn/trunk@303 59285afe-504e-ee2a-6240-25eb0d263adb
Added Match module to cabal file.

git-svn-id: https://trellys.googlecode.com/svn/trunk@304 59285afe-504e-ee2a-6240-25eb0d263adb
added some more constructions from the Altenkirch and McBride paper

git-svn-id: https://trellys.googlecode.com/svn/trunk@305 59285afe-504e-ee2a-6240-25eb0d263adb
added some more constructions from the Altenkirch and McBride paper

git-svn-id: https://trellys.googlecode.com/svn/trunk@306 59285afe-504e-ee2a-6240-25eb0d263adb
Added a flag to control printing of the AST when comparing types, until
pretty-printing is fixed.

git-svn-id: https://trellys.googlecode.com/svn/trunk@307 59285afe-504e-ee2a-6240-25eb0d263adb
Removing extra debugging statement.

git-svn-id: https://trellys.googlecode.com/svn/trunk@308 59285afe-504e-ee2a-6240-25eb0d263adb
made some minor changes to fin.sep

git-svn-id: https://trellys.googlecode.com/svn/trunk@309 59285afe-504e-ee2a-6240-25eb0d263adb
Fixed constructions so that arguments are wrapped in tcasts, if there is a
termination proof available.

git-svn-id: https://trellys.googlecode.com/svn/trunk@310 59285afe-504e-ee2a-6240-25eb0d263adb