Edwin Brady 04a0f5001f Correct multiplicities when checking Pi binders ... We've always just used 0, which isn't correct if the function is going to be used in a runtime pattern match. Now calculate correctly so that we're explicit about which type level variables are used at runtime. This might cause some programs to fail to compile, if they use functions that calculate Pi types. The solution is to make those functions explicitly 0 multiplicity. If that doesn't work, you may have been accidentally trying to use compile-time only data at run time! Fixes #1163		2021-03-09 17:23:05 +00:00
..
Control	[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) (#1095)	2021-02-24 11:07:16 +00:00
Data	Correct multiplicities when checking Pi binders	2021-03-09 17:23:05 +00:00
Debug	Back to HasIO, remove MonadIO	2020-06-21 19:21:22 +01:00
Decidable	Some cleanup was done. Changed code is mosly equivalent to the former.	2021-02-16 19:05:33 +00:00
Language	Fix import loading	2020-05-27 15:49:03 +01:00
Search	[ new ] Proof search from 'Applications of Applicative Proof Search' (#1093)	2021-03-01 08:29:43 +00:00
Syntax	Change PreorderReasoning arguments to 0	2021-02-14 15:12:17 +00:00
System	[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) (#1095)	2021-02-24 11:07:16 +00:00
Test	[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) (#1095)	2021-02-24 11:07:16 +00:00
Text	[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) (#1095)	2021-02-24 11:07:16 +00:00
contrib.ipkg	[ new ] Proof search from 'Applications of Applicative Proof Search' (#1093)	2021-03-01 08:29:43 +00:00
Makefile	Refactor makefiles	2020-05-19 18:50:47 +06:00