8 Commits

Author	SHA1	Message	Date
Denis Buzdalov	3ca065b85d	[ fix #2088 ] Make %runElab expression propagate its rig to check	2022-10-07 10:55:22 +02:00
Guillaume Allais	5631608782	[ base ] deriving Foldable	2022-09-24 10:20:25 +01:00
Guillaume Allais	6891490ed2	[ fix ] support for implicits in Deriving.Functor ... A lot of refactoring to bring these. That's hopefully the last feature that was needed...	2022-08-29 18:35:24 +01:00
Guillaume Allais	4672305fc3	[ fix ] more filtering of invalid datatypes	2022-08-13 11:29:19 +01:00
G. Allais	0cbbf97b79	[ new ] extend Deriving.Functor to (non-strictly) positive functors (#2591)	2022-07-18 14:10:46 +01:00
G. Allais	4874bf2114	[ fix ] handle implicit arguments in Deriving.Functor (#2572)	2022-07-07 09:55:13 +01:00
Guillaume Allais	7db20d38a3	[ cleanup ] Fewer assert_total in deriving Functor	2022-07-04 12:03:49 +01:00
G. Allais	aeeb338e6c	[ new ] deriving Functor (#2568)	2022-07-04 08:58:18 +01:00