Initial directory structure.

git-svn-id: https://trellys.googlecode.com/svn/trunk@1 59285afe-504e-ee2a-6240-25eb0d263adb
initial import of trellys project sources

git-svn-id: https://trellys.googlecode.com/svn/trunk@2 59285afe-504e-ee2a-6240-25eb0d263adb
added simple Makefile and more READMEs

git-svn-id: https://trellys.googlecode.com/svn/trunk@3 59285afe-504e-ee2a-6240-25eb0d263adb
moved single file from LangLib into src, to avoid conflicts with full LangLib install

git-svn-id: https://trellys.googlecode.com/svn/trunk@4 59285afe-504e-ee2a-6240-25eb0d263adb
merged the tickets.txt contents into the ticket system on google: two issues had already been fixed :)

git-svn-id: https://trellys.googlecode.com/svn/trunk@5 59285afe-504e-ee2a-6240-25eb0d263adb
changed svn:externals (that pulls in replib) to use old svn (to support old clients)

git-svn-id: https://trellys.googlecode.com/svn/trunk@7 59285afe-504e-ee2a-6240-25eb0d263adb
proper definition of recvec allows us to avoid the cast-shifting acrobatics

git-svn-id: https://trellys.googlecode.com/svn/trunk@9 59285afe-504e-ee2a-6240-25eb0d263adb
sorry, this is the corrected definition now

git-svn-id: https://trellys.googlecode.com/svn/trunk@10 59285afe-504e-ee2a-6240-25eb0d263adb
Updated to use r40 version of RepLib

git-svn-id: https://trellys.googlecode.com/svn/trunk@11 59285afe-504e-ee2a-6240-25eb0d263adb
Changing replib-read-only to be r40.

git-svn-id: https://trellys.googlecode.com/svn/trunk@12 59285afe-504e-ee2a-6240-25eb0d263adb
Implemented the new conv rule. The syntax is shown below. The implementation has been tested against the old test cases, but I have not tested against any actual uses of simulteneous conversions.

conv <expr> by <expr> (, <expr>)* at <identifier>+ . <expr>

git-svn-id: https://trellys.googlecode.com/svn/trunk@16 59285afe-504e-ee2a-6240-25eb0d263adb
Modified makefile to classify tests as 'expected pass' or 'expected fail'. A number of test cases are classifed as unknown. Please take a look, and if you see a test case that's misclassified, correct the classification.

git-svn-id: https://trellys.googlecode.com/svn/trunk@17 59285afe-504e-ee2a-6240-25eb0d263adb
Closed #1, error when comment at beginning of file.

Whitepace (and comments) now allowed before 'module' keyword.

git-svn-id: https://trellys.googlecode.com/svn/trunk@18 59285afe-504e-ee2a-6240-25eb0d263adb
Trying to use multi-conversion to prove append associates.

Getting a type error, where two types that are printed the same are not
equal.

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

git-svn-id: https://trellys.googlecode.com/svn/trunk@20 59285afe-504e-ee2a-6240-25eb0d263adb
Axioms for observational equivalence, plus a few demos.

git-svn-id: https://trellys.googlecode.com/svn/trunk@21 59285afe-504e-ee2a-6240-25eb0d263adb
Sigh. Just proved (\x.1) = (\x.0). Wonder how OTT is sound then.

git-svn-id: https://trellys.googlecode.com/svn/trunk@22 59285afe-504e-ee2a-6240-25eb0d263adb
Fixed a bug in typechecking contra.

git-svn-id: https://trellys.googlecode.com/svn/trunk@23 59285afe-504e-ee2a-6240-25eb0d263adb
Added a new flag to '-p' for 'picky equality' so that we can experiment with alternative definitions of equality. When typechecking with this flag enabled, all joins must be between terms of the same type and all conversions must be between terms of the same type. With this flag, Ott.trellys is rejected. (As are many other things.)

git-svn-id: https://trellys.googlecode.com/svn/trunk@24 59285afe-504e-ee2a-6240-25eb0d263adb
Rolling back edits to GenericBind that I didn't want to commit just yet.

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