6 Commits

Author	SHA1	Message	Date
Edwin Brady	c9b20911e1	Add linear pair/dependent pair to the prelude ... I'm playing with some linear structures and finding these useful a lot, so good to have a consistent syntax for it. '#' is chosen because it's short, looks a bit like a cross if you look at it from the right angle (!) and so as not to clash with '@@' in preorder reasoning syntax.	2020-06-12 11:18:12 +01:00
Mark Barbone	18c6c4a385	Clarify assert_{total,smaller} docs	2020-06-01 15:37:34 -04:00
Mark Barbone	58532a6a6c	Explain multiplicity 0 in assert_smaller docs	2020-06-01 15:37:34 -04:00
Mark Barbone	4bf2d11f6c	Add appropriate linearity annotation to assert_smaller and assert_total	2020-06-01 15:37:33 -04:00
Edwin Brady	222a6a7f31	More fine-grained assert_total in unpack ... If it's around the whole thing, it might drop out if unpack is partially evaluated by the unifier. It should be as fine grained as possible.	2020-05-24 19:13:24 +01:00
Edwin Brady	dec7dff622	Add libraries	2020-05-18 14:00:08 +01:00