[no description] http://git.yellowsquid.uk/yellowsquid/inky.git/atom?h=master 2024-10-28T15:34:16Z 2024-10-28T15:34:16Z Greg Brown greg.brown01@ed.ac.uk 2024-10-28T15:34:16Z urn:sha1:e258c78a5ab9529242b4c8fa168eda85430e641e Too few proofs were relevant. Now they are. 2024-09-09T10:33:45Z Greg Brown greg.brown01@ed.ac.uk 2024-09-09T10:33:45Z urn:sha1:3a23bd851fc1a5d6e161dabc8a13f06bc8544a1d - use De Bruijn, as Namely, Painless had more pain than promised; - remove higher-kinded types; - provide ill-typing predicates; - prove substitution respects ill-typing;