3 Commits

Author	SHA1	Message	Date
Edwin Brady	8d7fa5c642	Add a heuristic for sorting search results ... Sort by proportion of bound variables used, which is likely to get us the right answer quicker. The results are generated in batches of 16 (a completely arbitrary choice) then sorted.	2020-07-29 23:54:52 +01:00
Edwin Brady	7083f7ac13	Add a 'reject' count to :gd ... This gives the number of implementations to reject before accepting one. It's intended as a reasonably cheap way of giving multiple results from interactive editing (e.g. the vim mode, which goes via the REPL and --client rather than the IDE mode)	2020-07-27 14:56:16 +01:00
Edwin Brady	df635cf8d7	Add :psnext and :gdnext at the REPL ... These continue the search from :ps and :gd next respectively, giving the next search result until there are no more results. Correspondingly, added ':proof-search-next' and ':generate-def-next' in IDE mode, which continue the search from the previous ':proof-search' and ':generate-def' respectively.	2020-07-27 13:45:10 +01:00