Skip to content

Actions: UniMath/agda-unimath

Actions

Clean up caches generated by pull requests

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
clean-up.yaml
290 workflow runs
290 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

Negation of rational reals Clean up caches generated by pull requests #590: Pull request #1304 closed by fredrik-bakke
February 9, 2025 01:00 12s lowasser:neg-rational-real
lowasser:neg-rational-real
February 9, 2025 01:00 12s
Real numbers are dense Clean up caches generated by pull requests #589: Pull request #1287 closed by fredrik-bakke
February 9, 2025 00:55 20s lowasser:dense-reals
lowasser:dense-reals
February 9, 2025 00:55 20s
For x y : ℚ, x < y if and only if real-ℚ x < real-ℚ y Clean up caches generated by pull requests #588: Pull request #1293 closed by fredrik-bakke
February 9, 2025 00:51 16s lowasser:real-ineq-rat-reverse
lowasser:real-ineq-rat-reverse
February 9, 2025 00:51 16s
Similarity of real numbers Clean up caches generated by pull requests #587: Pull request #1301 closed by fredrik-bakke
February 9, 2025 00:46 13s lowasser:similar-reals
lowasser:similar-reals
February 9, 2025 00:46 13s
Avoid escaped code in headers for min and max Clean up caches generated by pull requests #586: Pull request #1299 closed by fredrik-bakke
February 9, 2025 00:24 15s lowasser:min-max-name-headers
lowasser:min-max-name-headers
February 9, 2025 00:24 15s
For x y : ℚ, x ≤ y if and only if real-ℚ x ≤ real-ℚ y Clean up caches generated by pull requests #585: Pull request #1303 closed by fredrik-bakke
February 9, 2025 00:20 13s lowasser:nonstrict-ineq-real-rat
lowasser:nonstrict-ineq-real-rat
February 9, 2025 00:20 13s
q : ℚ is in the lower cut of a real only if real-ℚ q is less than that real, and analogously for the upper cut Clean up caches generated by pull requests #584: Pull request #1302 closed by fredrik-bakke
February 8, 2025 23:35 13s lowasser:ineq-real-rat-iff
lowasser:ineq-real-rat-iff
February 8, 2025 23:35 13s
Similarity of subtypes is reflexive, transitive, and antisymmetric at the same universe level Clean up caches generated by pull requests #583: Pull request #1295 closed by fredrik-bakke
February 8, 2025 23:12 14s lowasser:similarity-subtypes
lowasser:similarity-subtypes
February 8, 2025 23:12 14s
Relationships between inequality, strict inequality, and their negations on reals Clean up caches generated by pull requests #582: Pull request #1288 closed by fredrik-bakke
February 8, 2025 22:57 13s lowasser:ineq-strict-ineq-real
lowasser:ineq-strict-ineq-real
February 8, 2025 22:57 13s
Functorial action of existential quantifications, and applications in real-numbers Clean up caches generated by pull requests #581: Pull request #1298 closed by fredrik-bakke
February 8, 2025 21:43 20s fredrik-bakke:functorial-action-exists
fredrik-bakke:functorial-action-exists
February 8, 2025 21:43 20s
Raising a real number's universe level Clean up caches generated by pull requests #580: Pull request #1286 closed by lowasser
February 8, 2025 21:41 11s lowasser:raise-real
lowasser:raise-real
February 8, 2025 21:41 11s
If q : ℚ is in the lower cut of a real, real-ℚ q is less than that real, and analogously for the upper cut Clean up caches generated by pull requests #579: Pull request #1294 closed by fredrik-bakke
February 8, 2025 21:39 13s lowasser:ineq-real-rat-cut
lowasser:ineq-real-rat-cut
February 8, 2025 21:39 13s
Riffle shuffles Clean up caches generated by pull requests #578: Pull request #1297 closed by fredrik-bakke
February 8, 2025 20:37 12s djspacewhale:riffle-shuffles
djspacewhale:riffle-shuffles
February 8, 2025 20:37 12s
Rename min and max operations for decidable total orders Clean up caches generated by pull requests #577: Pull request #1292 closed by fredrik-bakke
February 8, 2025 15:28 14s lowasser:rename-min-max
lowasser:rename-min-max
February 8, 2025 15:28 14s
Minimum operation on rational numbers Clean up caches generated by pull requests #576: Pull request #1290 closed by lowasser
February 7, 2025 20:55 13s lowasser:minimum-rational
lowasser:minimum-rational
February 7, 2025 20:55 13s
Minimum and maximum for decidable total orders Clean up caches generated by pull requests #575: Pull request #1291 closed by EgbertRijke
February 7, 2025 20:39 13s lowasser:total-min-max
lowasser:total-min-max
February 7, 2025 20:39 13s
Large poset of real numbers Clean up caches generated by pull requests #574: Pull request #1289 closed by fredrik-bakke
February 7, 2025 00:22 13s lowasser:large-poset-real
lowasser:large-poset-real
February 7, 2025 00:22 13s
For p q : ℚ, succ-ℚ p * q = q + (p * q) Clean up caches generated by pull requests #573: Pull request #1282 closed by fredrik-bakke
February 6, 2025 18:51 15s lowasser:succ-rat-mul
lowasser:succ-rat-mul
February 6, 2025 18:51 15s
Concatenation laws for strict and nonstrict inequality on the reals Clean up caches generated by pull requests #572: Pull request #1284 closed by fredrik-bakke
February 6, 2025 18:44 14s lowasser:concat-le-leq-real
lowasser:concat-le-leq-real
February 6, 2025 18:44 14s
Truncated law of excluded middle Clean up caches generated by pull requests #571: Pull request #1285 closed by lowasser
February 6, 2025 04:51 12s lowasser:trunc-lem
lowasser:trunc-lem
February 6, 2025 04:51 12s
Truncated law of excluded middle Clean up caches generated by pull requests #570: Pull request #1285 closed by lowasser
February 6, 2025 04:50 11s lowasser:trunc-lem
lowasser:trunc-lem
February 6, 2025 04:50 11s
Inequality in ℝ Clean up caches generated by pull requests #569: Pull request #1275 closed by EgbertRijke
February 6, 2025 01:05 17s lowasser:ineq-real
lowasser:ineq-real
February 6, 2025 01:05 17s
Successor and predecessor for ℚ Clean up caches generated by pull requests #568: Pull request #1283 closed by EgbertRijke
February 6, 2025 01:00 22s lowasser:succ-rat
lowasser:succ-rat
February 6, 2025 01:00 22s
Dedekind reals are arithmetically located Clean up caches generated by pull requests #567: Pull request #1273 closed by lowasser
February 5, 2025 23:52 14s lowasser:located-implies-arithmetically-located
lowasser:located-implies-arithmetically-located
February 5, 2025 23:52 14s
For p q : ℚ, succ-ℚ p * q = q + (p * q) Clean up caches generated by pull requests #566: Pull request #1282 closed by lowasser
February 5, 2025 23:52 17s lowasser:succ-rat-mul
lowasser:succ-rat-mul
February 5, 2025 23:52 17s