13 Commits

Author	SHA1	Message	Date
Denis Buzdalov	8038f0a0f9	[ refactoring ] Tiny changes following up the idris-lang/Idris2#830 ... Some zeroes in signatures, one simpler implementation and formatting.	2021-05-10 09:07:36 +01:00
Denis Buzdalov	583442b359	[ contrib ] Arithmetic on Fin (#830) ... Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>	2021-04-23 12:05:13 +01:00
Denis Buzdalov	941e3963fa	[ base ] DecEq implementations of Fin and Vect were exported publicly	2021-03-18 16:07:21 +00:00
G. Allais	cee7e38894	[ new ] Proof search from 'Applications of Applicative Proof Search' (#1093)	2021-03-01 08:29:43 +00:00
Denis Buzdalov	4f28b92a19	Zero quantities were added to some interface usages.	2021-02-12 20:51:13 +00:00
Denis Buzdalov	123fbb7f33	weakenN's n parameter was made to have zero quantity.	2021-02-09 14:15:59 +00:00
Denis Buzdalov	13cc27da1f	An alternative (Fin-based) indexing function was added for lists.	2020-12-04 19:09:05 +00:00
Nick Drozd	2ae6e06565	Simplify Fin	2020-07-07 10:48:23 +01:00
Nick Drozd	faabbfcea1	Add some Uninhabited implementations	2020-07-07 10:48:23 +01:00
Nick Drozd	7c923944ae	Add %default total to a few modules	2020-07-07 10:48:23 +01:00
Alex Gryzlov	cd443f24f6	various stdlib updates	2020-06-11 23:14:11 +02:00
Edwin Brady	c88bf7af8d	Fix import loading ... This was taking too long, and adding too many things, because it was going too deep in the name of having everything accessible at the REPL and for the compiler. So, it's done a bit differently now, only chasing everything on a "full" load (i.e., final load at the REPL) This has some effects: + As systems get bigger, load time gets better (on my machine, checking Idris.Main now takes 52s from scratch, down from 76s) + You might find import errors that you didn't previously get, because things were being imported that shouldn't have been. The new way is correct! An unfortunate effect is that sometimes you end up getting "undefined name" errors even if you didn't explicitly use the name, because sometimes a module uses a name from another module in a type, which then gets exported, and eventually needs to be reduced. This mostly happens because there is a compile time check that should be done which I haven't implemented yet. That is, public export definitions should only be allowed to use names that are also public export. I'll get to this soon.	2020-05-27 15:49:03 +01:00
Edwin Brady	dec7dff622	Add libraries	2020-05-18 14:00:08 +01:00