8 Commits

Author	SHA1	Message	Date
Denis Buzdalov	f58a96e420	[ papers ] Move a postulate to a required parameter	2022-10-01 15:11:26 +01:00
G. Allais	d1ae9d9fd5	[ papers ] Computing with Generic Trees (#2661)	2022-09-16 11:40:09 +01:00
G. Allais	bdf3833df5	[ new ] Auto in Agda (+ bonus) (#2541) ... * [ new ] Auto in Agda (+ bonus) * [ minor ] use DN for more readable terms	2022-06-16 09:35:45 +01:00
G. Allais	1011cc6162	[ papers ] Tychonoff (Part I) (#2332)	2022-02-24 11:12:53 +00:00
Guillaume Allais	56009ad3ac	[ cleanup ] silence warnings in libs	2022-02-02 11:09:03 +00:00
André Videla	208adb7202	[ linear ] add utilities for linear datastructures (#2293)	2022-02-01 21:22:16 +00:00
Guillaume Allais	3c63902d82	[ new ] Dependent Tagless Final	2022-01-27 17:26:52 +00:00
G. Allais	ec5afa5065	[ libs ] move propaganda out of contrib (#2213)	2022-01-25 12:25:55 +00:00