Edwin Brady
bf64f843aa
A bit more totality checking polish
...
Need to check for 'assert_total' in getRefs, and get Inf and Lazy the
right way around!
2019-06-25 12:57:49 +01:00
Edwin Brady
0a15c2cda1
Pay attention to visibility of names
...
Name lookup and search should ignore names which aren't visible (that
is, private names in another namespace)
2019-06-24 00:57:22 +01:00
Edwin Brady
c3a4360ee9
Add missing ipkg
2019-06-19 18:50:46 +01:00
Edwin Brady
02c2358093
Add missing Makefile
2019-06-19 18:49:53 +01:00
Edwin Brady
ecb5cb1e40
Don't keep running delayed elaborators
...
Also fix a bug where the elaborator state wasn't updated on completing
the delayed elaborator, which could cause issues with implicitly bound
names in particular.
2019-06-16 20:48:31 +01:00
Edwin Brady
4bc87b4c72
Some TTC/Delay fixes
...
Need to run delayed elaborators before binding implicits, since there
might be some inside the delayed elaborator. Also reorganise TTC
implementations so they're all in one place.
2019-06-16 13:47:20 +01:00
Edwin Brady
a7bf075c94
Get GlobalHint flag right
...
'True' means a default hint, which is only used if all else fails (and
is only really intended to get default Integer)
2019-06-15 12:42:35 +01:00
Edwin Brady
c121910298
Add 'base' libraries
2019-06-15 11:54:22 +01:00
Edwin Brady
772b098de0
The Prelude type checks!
2019-06-13 13:23:21 +01:00
