Edwin Brady
0d4db3ee75
Add 'force' and 'delay' as functions
...
Since Force and Delay are keywords now, these may help in higher order
cases in particular.
2020-07-01 11:35:27 +01:00
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
