Commit Graph

8 Commits

Author SHA1 Message Date
Edwin Brady
99dac56e1e Make sure matches are not too specific
i.e. if an argument has a polymorphic type, we shouldn't allow a
concrete type in its place
2019-06-29 19:28:04 +01:00
Edwin Brady
f5a5d01274 Turn lets to lambdas in hole environments
This works better when lifting lemmas, and ensures that the type of
everything will be shown and not normalised away
2019-06-16 23:10:32 +01:00
Edwin Brady
772b098de0 The Prelude type checks! 2019-06-13 13:23:21 +01:00
Edwin Brady
5a3aa3b13c Some fixes for as patterns, add them implicitly
Much of the effort in renaming is to make types of holes display more
nicely!
2019-06-09 23:12:11 +01:00
Edwin Brady
146c301f6c Change main program to be Idris2
With the --yaffle flag, you get the old behaviour which is to invoke the
checker for the core theory (and all the tests are updated appropriately
for this).
2019-06-09 11:58:29 +01:00
Edwin Brady
3e3c224bcb Move some tests around
Add a 'search' category
2019-05-26 11:34:02 +01:00
Edwin Brady
8081b0374a First attempt at linearity checking pass
This slows things down a bit because to find the holes and give them the
right multiplicities, we need to normalise all the arguments which might
have been metavariables. Maybe we should skip this if we're not using
anything linear, for efficiency?

As patterns are handled by deciding which side of the as is considered
'used'. In case blocks, that should be the variable name, but in general
it should be the pattern, so IAs now has a flag to say which one.
2019-05-19 20:24:14 +01:00
Edwin Brady
411b8ccc07 Support eta in unification
Also added (necessarily) a rule for lambdas
2019-05-07 15:06:00 +01:00