Skip to content

Actions: UniMath/agda-unimath

Actions

Profile Library Typechecking

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
profiling.yaml
191 workflow runs
191 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

Large poset of real numbers (#1289) Profile Library Typechecking #191: Commit f335df0 pushed by fredrik-bakke
February 7, 2025 00:22 12m 8s master
master
February 7, 2025 00:22 12m 8s
For p q : ℚ, succ-ℚ p * q = q + (p * q) (#1282) Profile Library Typechecking #190: Commit 8662d37 pushed by fredrik-bakke
February 6, 2025 18:51 17m 27s master
master
February 6, 2025 18:51 17m 27s
Concatenation laws for strict and nonstrict inequality on the reals (… Profile Library Typechecking #189: Commit 8440b84 pushed by fredrik-bakke
February 6, 2025 18:44 12m 7s master
master
February 6, 2025 18:44 12m 7s
Inequality in ℝ (#1275) Profile Library Typechecking #188: Commit c6b929a pushed by EgbertRijke
February 6, 2025 01:05 21m 12s master
master
February 6, 2025 01:05 21m 12s
Successor and predecessor for ℚ (#1283) Profile Library Typechecking #187: Commit f21dcf3 pushed by EgbertRijke
February 6, 2025 01:00 12m 36s master
master
February 6, 2025 01:00 12m 36s
Make supertype implicit in raise-subtype (#1281) Profile Library Typechecking #186: Commit 83e7741 pushed by EgbertRijke
February 5, 2025 22:59 12m 14s master
master
February 5, 2025 22:59 12m 14s
Negation reverses strict inequality on ℝ (#1276) Profile Library Typechecking #185: Commit eb58aa1 pushed by EgbertRijke
February 5, 2025 22:47 12m 7s master
master
February 5, 2025 22:47 12m 7s
Raise subtypes to a universe level (#1277) Profile Library Typechecking #184: Commit 260f8ac pushed by EgbertRijke
February 5, 2025 22:14 16m 38s master
master
February 5, 2025 22:14 16m 38s
ℝ is unbounded (#1278) Profile Library Typechecking #183: Commit 065c73c pushed by EgbertRijke
February 5, 2025 22:05 12m 24s master
master
February 5, 2025 22:05 12m 24s
Decide for natural numbers whether x < y or y ≤ x (#1279) Profile Library Typechecking #182: Commit 26f7289 pushed by EgbertRijke
February 5, 2025 21:42 12m 28s master
master
February 5, 2025 21:42 12m 28s
Complementation reverses subtype containment (#1274) Profile Library Typechecking #181: Commit cf75821 pushed by EgbertRijke
February 5, 2025 20:37 22m 54s master
master
February 5, 2025 20:37 22m 54s
Strict inequality on the reals (#1272) Profile Library Typechecking #180: Commit c8d1edb pushed by EgbertRijke
February 5, 2025 20:28 18m 48s master
master
February 5, 2025 20:28 18m 48s
Inverses in groups are unique (#1271) Profile Library Typechecking #179: Commit 982c5b1 pushed by EgbertRijke
February 5, 2025 20:22 13m 0s master
master
February 5, 2025 20:22 13m 0s
Reassociated conjugation is the identity (#1270) Profile Library Typechecking #178: Commit 417b6f8 pushed by EgbertRijke
February 5, 2025 17:14 12m 42s master
master
February 5, 2025 17:14 12m 42s
For p : ℚ⁺, there is r : ℚ⁺ with r + r < p (#1269) Profile Library Typechecking #177: Commit ffc0501 pushed by EgbertRijke
February 5, 2025 15:01 12m 31s master
master
February 5, 2025 15:01 12m 31s
Archimedean property of ℚ (#1268) Profile Library Typechecking #176: Commit f7d9a5c pushed by EgbertRijke
February 4, 2025 22:59 12m 13s master
master
February 4, 2025 22:59 12m 13s
Negation on real numbers (#1246) Profile Library Typechecking #175: Commit 0b11fe7 pushed by EgbertRijke
February 4, 2025 22:44 12m 8s master
master
February 4, 2025 22:44 12m 8s
Rename wild higher categories (#1233) Profile Library Typechecking #174: Commit da15ec1 pushed by EgbertRijke
February 4, 2025 21:04 13m 40s master
master
February 4, 2025 21:04 13m 40s
Inclusion of ℤ in ℚ preserves addition (#1265) Profile Library Typechecking #173: Commit 1e542d8 pushed by EgbertRijke
February 4, 2025 20:54 12m 18s master
master
February 4, 2025 20:54 12m 18s
Archimedean property of fraction-ℤ (#1261) Profile Library Typechecking #172: Commit fb4dd23 pushed by EgbertRijke
February 4, 2025 16:38 19m 45s master
master
February 4, 2025 16:38 19m 45s
Subtracting positive rationals is a strictly deflationary map (#1266) Profile Library Typechecking #171: Commit bd003ab pushed by EgbertRijke
February 4, 2025 16:33 12m 11s master
master
February 4, 2025 16:33 12m 11s
Lossy unification on arithmetically located cuts (#1263) Profile Library Typechecking #170: Commit cafbf65 pushed by fredrik-bakke
February 4, 2025 00:12 12m 48s master
master
February 4, 2025 00:12 12m 48s
Reflective global subuniverses (#1228) Profile Library Typechecking #169: Commit 2ade811 pushed by EgbertRijke
February 3, 2025 22:54 15m 56s master
master
February 3, 2025 22:54 15m 56s
Existential quantification for the Archimedean property (#1262) Profile Library Typechecking #168: Commit 8868689 pushed by EgbertRijke
February 3, 2025 18:51 16m 5s master
master
February 3, 2025 18:51 16m 5s
Arithmetically located Dedekind cuts (#1257) Profile Library Typechecking #167: Commit 35df026 pushed by EgbertRijke
February 2, 2025 18:30 15m 44s master
master
February 2, 2025 18:30 15m 44s