yellowsquid/inky.git/src/Inky/Type, branch master [no description] http://git.yellowsquid.uk/yellowsquid/inky.git/atom?h=master 2025-03-13T13:20:29Z Modify definition of data types. 2025-03-13T13:20:29Z Greg Brown greg.brown01@ed.ac.uk 2025-01-30T16:57:47Z urn:sha1:f5b75edd91389f0a45045b707abfa36c746e8d54 Add quotation to help metaprogramming. 2025-01-07T13:50:13Z Greg Brown greg.brown01@ed.ac.uk 2025-01-07T13:50:13Z urn:sha1:f2490f5ca35b528c7332791c6932045eb9d5438b Add compilation to scheme. 2024-11-15T15:44:30Z Greg Brown greg.brown01@ed.ac.uk 2024-11-15T15:44:30Z urn:sha1:3caa95a139538bb07c74847ca3aba2603a03c502 Extract parser as an independent project. Write a fuelled reducer for System T. 2024-10-29T18:58:45Z Greg Brown greg.brown01@ed.ac.uk 2024-10-29T18:58:45Z urn:sha1:82783476f330801b54402bdcc4723add44a963dc Improve pretty printer. 2024-10-28T17:30:38Z Greg Brown greg.brown01@ed.ac.uk 2024-10-28T17:30:38Z urn:sha1:cd5d7c8207447a1a2dc78554288912d1950c9bf9 Make everything relevant. 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. Do a lot. 2024-10-09T15:26:23Z Greg Brown greg.brown01@ed.ac.uk 2024-10-09T15:26:23Z urn:sha1:8b326bb4a879be72cb6382519350cbb5231f7a6e - Add type aliases. - Make `suc` a symbol. - Fix incorrect specification for `IsFunction`. - Write parser for terms. - Use `collie` to improve command line experience. Introduce names in contexts. 2024-09-17T16:09:41Z Greg Brown greg.brown01@ed.ac.uk 2024-09-17T16:09:41Z urn:sha1:974717f0aa46bb295d44e239594b38f63f39ceab Introduce rows for n-ary sums and products. Remove union types. Define pretty printers for terms and types. 2024-09-13T14:17:52Z Greg Brown greg.brown01@ed.ac.uk 2024-09-13T14:17:52Z urn:sha1:33fc608bf9e44e814ba594c8a5d8294572966cbc