[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Remove obsolete tests



Removed a bunch of tests involving translating TIP to Haskell, then
converting that manually into Isabelle types, etc. Basically, a fragile
and over-engineered approach, compared to pulling types out of the
generated Isabelle.

I've left a test about finding equations for + and * from a theory of
naturals, since that's a decent thing to test. However, it won't work
as-is and it should also be put somewhere more appropriate, e.g. as a
dependency of isacosy or something.