12 Commits

Author	SHA1	Message	Date
G. Allais	f96c5ca596	[ papers ] LambdaPi (#2780)	2022-12-01 13:48:48 +00:00
Guillaume Allais	8556c81014	[ new ] typed ABT	2022-11-04 16:20:46 +00:00
G. Allais	fd46e31da3	[ new ] typed Krivine (#2749)	2022-11-04 10:05:31 +00:00
G. Allais	ad817538e0	[ new ] typed SECD (#2743)	2022-11-02 12:58:13 +00:00
G. Allais	ee8113bb9d	[ papers ] A Completely Unique Account of Enumeration (#2659)	2022-11-01 16:31:57 +00:00
Stefan Höck	85ddafbac5	[ fix ] bump version of linear and papers packages (#2735)	2022-10-28 08:55:35 +01:00
Thomas E. Hansen	d5c9253e7e	[ papers ] Fix impl.n s.t. model-checking Peterson's works ... Thanks to the debug info supplied by #2673, I was able to spot which functions were blocking and `public import` the relevant files in `papers/Search/Properties.idr`. As a result the GCL file now type-checks, albeit extremely slowly! I stopped an evaluation of `petersonsCorrect` at the REPL after 15 minutes and ~14GB of RAM consumed.	2022-10-05 14:30:08 +02: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	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