|
aea11ac62f
|
merge
|
2024-01-30 13:44:08 +01:00 |
|
|
78260e3f91
|
refactor to support newest agda-categories release
|
2024-01-29 18:15:06 +01:00 |
|
|
8241082f3f
|
updated agda-cat
|
2024-01-29 15:42:18 +01:00 |
|
|
2dc6420a35
|
sync
|
2024-01-29 15:38:50 +01:00 |
|
|
f0923f1007
|
finished congruence proof
|
2024-01-29 12:52:25 +01:00 |
|
|
11dd7f8f23
|
sync
|
2024-01-28 15:07:38 +01:00 |
|
|
7568f60833
|
Refactor to update library versions
|
2024-01-25 13:30:41 +01:00 |
|
|
6ba246ee53
|
updated library versions
|
2024-01-24 15:22:54 +01:00 |
|
|
577b095325
|
sync
|
2024-01-16 10:07:01 +01:00 |
|
|
5557dd1d6a
|
changed definition
|
2024-01-14 13:00:56 +01:00 |
|
|
291b33abbe
|
some renaming and new definitions
|
2024-01-14 12:20:49 +01:00 |
|
|
2cc26eeb9a
|
cleanup and add uniformity proof
|
2024-01-13 19:39:16 +01:00 |
|
|
202d130d33
|
Finish subproof
|
2024-01-10 17:46:55 +01:00 |
|
|
a6fd66ef29
|
sync
|
2024-01-09 16:02:09 +01:00 |
|
|
9beebd009d
|
Some progress
|
2024-01-09 13:34:53 +01:00 |
|
|
8e6e1d01cd
|
minor and add sergeys suggestion
|
2024-01-08 12:57:33 +01:00 |
|
|
4aaf6ff164
|
minor
|
2024-01-07 18:09:45 +01:00 |
|
|
45d281fc5a
|
fixed definition of iter
|
2024-01-07 15:55:54 +01:00 |
|
|
f93083706b
|
progress
|
2024-01-05 18:56:30 +01:00 |
|
|
32c479a027
|
Finish delayMonad proofs without musical notation
|
2024-01-05 17:51:20 +01:00 |
|
|
197d036d42
|
Work on Delay Monad without musical notation
|
2024-01-04 18:01:17 +01:00 |
|
|
fd7b498554
|
sync
|
2024-01-03 14:41:35 +01:00 |
|
|
4d24b1d0e5
|
minor comments (+ fix makefile)
|
2023-12-22 19:41:00 +01:00 |
|
|
f5ae9924eb
|
continue refactor
|
2023-12-22 17:54:11 +01:00 |
|
|
395f548334
|
♻ major refactor of example
|
2023-12-21 14:22:18 +01:00 |
|
|
7265de98d0
|
sync
|
2023-12-21 10:39:01 +01:00 |
|
|
327c333293
|
minor
|
2023-12-20 18:14:54 +01:00 |
|
|
d35498e1fa
|
minor
|
2023-12-20 18:08:35 +01:00 |
|
|
59b105823f
|
minor refactor
|
2023-12-19 16:01:18 +01:00 |
|
|
c848184732
|
minor
|
2023-12-17 20:08:26 +01:00 |
|
|
6f616f58f5
|
re-add IsFreeObject, work on proof that delay is freeelgot
|
2023-12-15 18:05:58 +01:00 |
|
|
5f1ab060bb
|
Work on example
|
2023-12-14 19:11:20 +01:00 |
|
|
7bd77a4f47
|
Progress on proof that delay is preElgot
|
2023-12-14 14:40:38 +01:00 |
|
|
17ecc55223
|
Work on delay monad
|
2023-12-13 20:53:33 +01:00 |
|
|
4c3f3923a1
|
work on delayh
|
2023-12-08 22:03:23 +01:00 |
|
|
7ec344dfeb
|
minor
|
2023-12-07 18:54:15 +01:00 |
|
|
59f60810e7
|
minor
|
2023-12-06 09:16:10 +01:00 |
|
|
64c4a4263d
|
Work on delay example
|
2023-12-05 20:52:53 +01:00 |
|
|
be0971ae42
|
Fixed folder structure
|
2023-12-05 18:07:06 +01:00 |
|