3 Commits

Author	SHA1	Message	Date
Guillaume ALLAIS	a9ff13c663	[ new ] proof that evaluation is Domain-independent	2020-10-29 23:05:41 +00:00
Guillaume ALLAIS	482527063c	[ new ] Variant with a runtime irrelevant Domain ... Rather than translating the constraints to a Dybjer-Setzer IR code we can produce an ad-hoc definition of a `Domain` that we will be able to make runtime irrelevant. This means that compiled code will never need to construct a proof that a value is in the domain of the function: it will simply run the function!	2020-10-15 17:03:32 +01:00
Guillaume ALLAIS	864be2c9dc	[ contrib ] add McBride's General monad	2020-10-15 17:03:32 +01:00