yellowsquid/idris-obs.git/src/Obs/Typing, branch master [no description] http://git.yellowsquid.uk/yellowsquid/idris-obs.git/atom?h=master 2023-01-08T00:56:11Z Add box types. 2023-01-08T00:56:11Z Greg Brown greg.brown01@ed.ac.uk 2023-01-08T00:56:11Z urn:sha1:9af1a41a58575508c8d2dff6e7b25a5caac8aadc Add postulates. 2023-01-07T22:01:05Z Greg Brown greg.brown01@ed.ac.uk 2023-01-07T22:01:05Z urn:sha1:eb49ef28b93431d9694a17b1ad44d9ea966bcb05 Add containers types. 2023-01-07T21:58:30Z Greg Brown greg.brown01@ed.ac.uk 2023-01-07T21:10:30Z urn:sha1:ff65d1e285a97295708899bebdcc83ec214cd347 Containers are syntactic sugar. They are also completely untested. Add more program structure to normal forms. 2023-01-05T17:06:33Z Greg Brown greg.brown01@ed.ac.uk 2023-01-05T17:06:33Z urn:sha1:06bd13433cb5e7edcff551454107c9d4e4d88f8f Add more program structure to type universes. 2023-01-02T15:43:24Z Greg Brown greg.brown01@ed.ac.uk 2023-01-02T15:43:24Z urn:sha1:74f0dc953839179aae071dda1ddb924295bc6061 Index normal forms with relevance. 2023-01-01T12:11:50Z Greg Brown greg.brown01@ed.ac.uk 2023-01-01T12:11:50Z urn:sha1:7e184c20d545afb55f6e962b8bfea882b23699fa - Remove container types. - Replace sum types with booleans. - Remove type annotation from absurd. - Add original type as argument to cast. - Make if (was case) take a lambda for the return type. Add Container types. 2022-12-22T00:02:23Z Greg Brown greg.brown01@ed.ac.uk 2022-12-22T00:02:23Z urn:sha1:02cb45707da07d5e6faca92158d10a6e454a6bac Add sum types. 2022-12-21T20:32:56Z Greg Brown greg.brown01@ed.ac.uk 2022-12-21T20:32:56Z urn:sha1:a8a4ef9933a1a07b6fbf2d257df2a5fb40b1e87d