feat: more API about order types #33420

YanYablonovskiy · 2025-12-31T05:38:32Z

Adding OrderTypes, equivalence classes of linear orders up to order isomorphism.

depends on: feat(Order): order types #34034

github-actions · 2025-12-31T05:39:43Z

PR summary b79634a5c1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Order.Types.Defs` (new file)	137
`Mathlib.Order.Types.Basic` (new file)	537

Declarations diff

+ OrderType
+ OrderType.instSetoid
+ _root_.RelIso.orderType_eq
+ bot_eq_zero
+ card
+ card_le_card
+ card_mono
+ card_one
+ card_type
+ card_zero
+ emptySumLex
+ emptySumLex_apply_inr
+ eta
+ inductionOn
+ inductionOn₂
+ inductionOn₃
+ inhabited
+ instNeZeroOne
+ instOrdBot
+ instance (n : Nat) : OfNat OrderType n
+ instance (o : OrderType) : LinearOrder o.ToType
+ instance : Add OrderType.{u}
+ instance : AddMonoid OrderType
+ instance : HAdd OrderType.{u} OrderType.{v} OrderType.{max u v}
+ instance : HMul OrderType.{u} OrderType.{v} OrderType.{max u v}
+ instance : LeftDistribClass OrderType
+ instance : Monoid OrderType
+ instance : Mul OrderType
+ instance : One OrderType
+ instance : Preorder OrderType
+ instance : ZeroLEOneClass OrderType
+ isEmpty_toType_iff
+ isEmpty_toType_zero
+ liftOn
+ liftOn_type
+ nonempty_toType_iff
+ nontrivial
+ not_lt_zero
+ ofIsEmpty
+ one_def
+ one_ne_zero
+ pos_iff_ne_zero
+ prodAssoc
+ prodLexAssoc
+ prodLexCongr
+ sumLexEmpty
+ sumLexEmpty_apply_inl
+ sumLexProdLexDistrib
+ theta
+ type
+ type_add
+ type_eq
+ type_eq_one
+ type_eq_zero
+ type_le_type
+ type_le_type_iff
+ type_mul
+ type_ne_zero
+ type_ne_zero_iff
+ type_of_isEmpty
+ type_of_unique
+ type_toType
+ zero
+ zero_le

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

vihdzp

Thanks for working on this! I've got lots of small suggestions/improvements, and a few larger ones.

Mathlib/Order/OrderType.lean

vihdzp

Thanks for working on this! I've got lots of small suggestions/improvements, and a few larger ones.

Mathlib/Order/OrderType.lean

YaelDillies · 2025-12-31T09:32:11Z

Mathlib/Order/OrderType.lean

+/-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. -/
+def omega0 : OrderType := type ℕ
+
+/-- The order type of the rational numbers. -/
+def eta : OrderType := type ℚ
+
+/-- The order type of the real numbers on the interval `(0,1)`. -/
+def theta : OrderType := type (Set.Ioo (0 : ℝ) 1)


Would be good to double-check these notations are the literature-approved ones

I can vouch for omega and eta, I'd have to check for theta.

Also surely type (Set.Ioo (0 : ℝ) 1) = type ℝ, no?

YaelDillies · 2025-12-31T09:32:47Z

Mathlib/Order/OrderType.lean

+Copyright (c) _
+-/
+import Mathlib.SetTheory.Cardinal.Basic
+import Mathlib.SetTheory.Ordinal.Basic


We already talked about this, but IMO ordinals should import order types, not the other way around

vihdzp · 2026-01-01T11:35:35Z

(once you've applied all/most suggestions, remove the awaiting author tag and please make sure to notify me!)

YanYablonovskiy · 2026-01-04T11:30:39Z

(once you've applied all/most suggestions, remove the awaiting author tag and please make sure to notify me!)

@vihdzp I believe i have addressed almost all of the points, some things still need to be moved but the monoid definition prevents imports of Ordertype from cardinal (for now) , and certain missing instances made it hard to move the empty sum order iso parts.

The other file changes will be made into separate small PRs i imagine.

YanYablonovskiy · 2026-01-04T12:20:53Z

-awaiting-author

YaelDillies

Could you make a preliminary PR for the order isos?

Mathlib/Order/Hom/Basic.lean

Mathlib/Order/OrderType.lean

YaelDillies · 2026-01-04T16:04:01Z

Mathlib/Order/OrderType.lean

+/-- An auxiliary structure representing a linearly ordered type. -/
+@[ext]
+structure LinearOrderedType : Type (u + 1) where
+  carrier : Type u
+  le : LE carrier
+  isLinearOrder_carrier : Std.IsLinearOrder carrier


What's the reason not to use LinOrd here?

I suggested this design and gave an argument against LinOrd in this reply. In particular:

I think the categorical properties of LinOrd are irrelevant here.

~~We don't need the extra structure that LinearOrder comes bundled with to define an order type.~~ Don't agree with this part anymore, see here.

I think the categorical properties of LinOrd are irrelevant here.

Sure, but we are free to ignore those categorical properties? I am worried about two definitions doing the exact same thing.

LinOrd is a category of mathematical interest. LinearOrderedType is an auxiliary structure which should have no public API that exists only to declare a much more interesting quotient on. Compare WellOrder.

Mathlib/Order/OrderType.lean

Mathlib/Order/Hom/Basic.lean

Mathlib/Order/Hom/Lex.lean

Mathlib/Order/OrderType.lean

vihdzp · 2026-01-04T19:17:27Z

You know, I thought about the Std.IsLinearOrder thing a bit more, and I'm no longer sure that was a good idea. I looked throughout the code for examples of using Ordinal.type on anything that didn't already have a LinearOrder + WellFoundedLT instance and found nothing. We do care about the rank function in general well-founded relations (which is what I was remembering), but that can be implemented regardless.

So yeah, I think we could just define OrderType as a quotient of LinearOrders, and later redefine Ordinal.type so that it accepts only a LinearOrder + WellFoundedLT type rather than an unbundled IsWellOrdered relation. In fact, we could very well deprecate the IsWellOrder typeclass altogether.

But maybe wait for Yaël's opinion before you change anything, I don't want you to have to undo your work all over again!

Mathlib/Order/Hom/Basic.lean

YaelDillies · 2026-01-05T08:01:34Z

wait for Yaël's opinion before you change anything

I do think we should use LinearOrder here. Furthermore, I don't buy the argument that we shouldn't use LinOrd. If your issue with it is that it would needlessly import category theory, then we should split the file where it is defined into a category-less part.

vihdzp · 2026-01-05T08:05:49Z

All we actually need from LinOrd is the definition. But if we can move it out into some defs file then sure, we might as well use it.

YaelDillies · 2026-01-05T08:09:36Z

I think it's reasonable to move it to Order.Defs

YanYablonovskiy · 2026-01-05T14:13:07Z

Order/Type/... ended up highlighting Type as a keyword, Types sounds strange. Order/OrderType is echoing Order. So not sure what to name it.

YanYablonovskiy · 2026-01-05T14:13:26Z

-awaiting-author

vihdzp

Small nitpicks of mine. This PR is shaping up quite nicely!

You could already start properly PRing the first pieces of this. The material on Order.Hom looks quite good (modulo some small suggestions) and I'd like to use it to golf the analogous proofs on Ordinal. You could then PR the Order.Types.Defs file, and at that point we can start thinking about what kind of API to add where and how to eventually link this to Ordinal.

Mathlib/Order/Defs/LinearOrder.lean

vihdzp · 2026-01-05T18:38:49Z

Mathlib/Order/Types/Defs.lean

@@ -0,0 +1,229 @@
+/-


I think Type would be a better name for the folder. We generally don't pluralize names of mathematical objects in the file structure (we have Order.CompleteSublattice say, rather than Order.CompleteSublattices).

or OrderType?

The Order part of OrderType seems redundant given that we're already in the Order folder.

But Order.Type sounds like it should be about order properties of Type

I guess we can also just keep the folder named Order.Types. Matches ModelTheory.Types, for instance.

Mathlib/Order/Types/Defs.lean

vihdzp · 2026-01-05T19:06:26Z

Mathlib/Order/Types/Defs.lean

+  le_trans a b c :=
+    Quotient.inductionOn₃ a b c fun _ _ _ ⟨f⟩ ⟨g⟩ ↦ ⟨f.trans g⟩
+
+instance instNeZeroOne : NeZero (1 : OrderType) :=


I'd rather not be naming instances unless we have a legitimate reason to.

Suggested change

instance instNeZeroOne : NeZero (1 : OrderType) :=

instance : NeZero (1 : OrderType) :=

Disagree. I'd rather make sure the instances can be found by name

Is the default name given here a bad one?

Mathlib/Order/Types/Defs.lean

Mathlib/Order/Types/Basic.lean

vihdzp · 2026-01-05T19:38:26Z

Mathlib/Order/Types/Basic.lean

+  add := Quotient.map₂ (fun r s ↦ ⟨(r ⊕ₗ s)⟩)
+   fun _ _ ha _ _ hb ↦ ⟨OrderIso.sumLexCongr (Classical.choice ha) (Classical.choice hb)⟩
+
+instance : HAdd OrderType.{u} OrderType.{v} OrderType.{max u v} where


I (re)opened a Zulip thread about this: #mathlib4 > Universe-heterogeneous ordinal and cardinal relations @ 💬

Mathlib/Order/Types/Basic.lean

vihdzp · 2026-01-05T19:40:25Z

Mathlib/Order/Types/Basic.lean

+def eta : OrderType := type ℚ
+
+/-- The order type of the real numbers. -/
+def theta : OrderType := type ℝ


I'll reiterate my suggestion that I'd like to see this in another file, probably one dedicated to η-orders entirely. We shouldn't be importing the real numbers on what's really quite basic order theory.

vihdzp · 2026-01-05T19:47:43Z

🌶️ take incoming: should we eventually move the Ordinal folder to Order or even to Order.Type? It feels kind of silly to categorize it as "set theory" when our development is not even based on ZFC sets. And it'd be nice to keep these parallel developments (general order types, ordinals) close together.

YanYablonovskiy · 2026-01-06T08:38:59Z

Still need to move some of the OrderTypes , and will open a seperate pr for the OrderIso/Lex lemmas.

-awaiting-author

commit d51b84d Author: YanYablonovskiy <[email protected]> Date: Tue Jan 6 20:13:26 2026 +1100 OrderIso prod lemmas adjustment commit 4c41035 Merge: b88c734 15f6691 Author: Yan Yablonovskiy <[email protected]> Date: Tue Jan 6 20:04:32 2026 +1100 Merge branch 'master' into master commit b88c734 Author: YanYablonovskiy <[email protected]> Date: Tue Jan 6 19:33:15 2026 +1100 Changes from review commit 8252446 Author: Yan Yablonovskiy <[email protected]> Date: Tue Jan 6 16:00:09 2026 +1100 Apply suggestions from code review Co-authored-by: Violeta Hernández Palacios <[email protected]> commit 8ac8458 Author: YanYablonovskiy <[email protected]> Date: Tue Jan 6 01:11:04 2026 +1100 Change mathlib imports from `OrderType` `OrderType.lean` no longer exists commit f353fe8 Merge: 30bd77d 959c852 Author: Yan Yablonovskiy <[email protected]> Date: Mon Jan 5 23:17:21 2026 +1100 Merge branch 'leanprover-community:master' into master commit 30bd77d Author: YanYablonovskiy <[email protected]> Date: Mon Jan 5 21:49:57 2026 +1100 Refactor as per suggestions, back to `LinOrd` commit f8cd844 Merge: f04b327 a57b343 Author: YanYablonovskiy <[email protected]> Date: Mon Jan 5 21:49:30 2026 +1100 Merge branch 'master' of https://github.com/YanYablonovskiy/mathlib4_Order-types-Issue28278 commit f04b327 Author: YanYablonovskiy <[email protected]> Date: Mon Jan 5 11:36:50 2026 +1100 Apply suggestions commit a57b343 Merge: 5937b50 8c8bf56 Author: Yan Yablonovskiy <[email protected]> Date: Mon Jan 5 11:30:56 2026 +1100 Merge branch 'leanprover-community:master' into master commit 5937b50 Merge: 07abc73 2330302 Author: YanYablonovskiy <[email protected]> Date: Mon Jan 5 10:21:08 2026 +1100 Merge branch 'master' of https://github.com/YanYablonovskiy/mathlib4_Order-types-Issue28278 commit 2330302 Author: Yan Yablonovskiy <[email protected]> Date: Mon Jan 5 10:20:45 2026 +1100 Apply suggestions from code review Co-authored-by: Yaël Dillies <[email protected]> Co-authored-by: Violeta Hernández Palacios <[email protected]> commit 07abc73 Author: YanYablonovskiy <[email protected]> Date: Mon Jan 5 00:44:02 2026 +1100 Fix recommended_spellings commit b25cb4c Author: YanYablonovskiy <[email protected]> Date: Mon Jan 5 00:37:52 2026 +1100 Add doc-string and some more typos commit 067b8cd Author: YanYablonovskiy <[email protected]> Date: Mon Jan 5 00:31:32 2026 +1100 Minor typos commit 4b5a837 Author: YanYablonovskiy <[email protected]> Date: Sun Jan 4 22:26:24 2026 +1100 Finish conversation review suggestions commit 5429c1b Author: Yan Yablonovskiy <[email protected]> Date: Fri Jan 2 23:31:29 2026 +1100 Apply suggestions from code review [skip ci] Co-authored-by: Yaël Dillies <[email protected]> Co-authored-by: Violeta Hernández Palacios <[email protected]> commit 630f0ea Author: YanYablonovskiy <[email protected]> Date: Fri Jan 2 23:14:37 2026 +1100 Style fix commit bf5166d Author: YanYablonovskiy <[email protected]> Date: Fri Jan 2 22:58:10 2026 +1100 Fix module error commit 2f0a005 Merge: 44753fe 519f454 Author: Yan Yablonovskiy <[email protected]> Date: Fri Jan 2 20:11:02 2026 +1100 Merge branch 'leanprover-community:master' into master commit 44753fe Author: YanYablonovskiy <[email protected]> Date: Fri Jan 2 19:42:27 2026 +1100 Bump commit 43b7d68 Author: YanYablonovskiy <[email protected]> Date: Fri Jan 2 19:18:34 2026 +1100 Clean up imports, get rid of sorries, and address some comments commit f888e2b Author: YanYablonovskiy <[email protected]> Date: Thu Jan 1 22:12:33 2026 +1100 Update OrderType.lean Add copyright [skip actions] commit 9848662 Author: YanYablonovskiy <[email protected]> Date: Thu Jan 1 21:56:01 2026 +1100 Update OrderType.lean commit b8acc2e Author: Yan Yablonovskiy <[email protected]> Date: Thu Jan 1 20:15:25 2026 +1100 Apply suggestions from code review Co-authored-by: Violeta Hernández Palacios <[email protected]> Co-authored-by: Yaël Dillies <[email protected]> commit a5e62be Merge: 6aa39b3 de80207 Author: YanYablonovskiy <[email protected]> Date: Wed Dec 31 16:34:44 2025 +1100 Merge branch 'master' of https://github.com/YanYablonovskiy/mathlib4_Order-types-Issue28278 commit 6aa39b3 Author: YanYablonovskiy <[email protected]> Date: Wed Dec 31 16:34:33 2025 +1100 Update OrderType.lean commit de80207 Merge: 669a1d3 6dc6d70 Author: Yan Yablonovskiy <[email protected]> Date: Wed Dec 31 16:34:24 2025 +1100 Merge branch 'leanprover-community:master' into master commit 669a1d3 Merge: a90d529 6371049 Author: Yan Yablonovskiy <[email protected]> Date: Mon Dec 29 10:38:08 2025 +1100 Merge branch 'leanprover-community:master' into master commit a90d529 Merge: 24bb5b0 cc5691d Author: Yan Yablonovskiy <[email protected]> Date: Mon Dec 22 13:06:26 2025 +1100 Merge branch 'leanprover-community:master' into master commit 24bb5b0 Merge: 4985680 5334b1e Author: Yan Yablonovskiy <[email protected]> Date: Wed Nov 26 18:44:18 2025 +1100 Merge branch 'leanprover-community:master' into master commit 4985680 Merge: 711df94 3f87ea8 Author: Yan Yablonovskiy <[email protected]> Date: Sun Nov 23 12:48:18 2025 +1100 Merge branch 'leanprover-community:master' into master commit 711df94 Merge: 6534400 b3cf7a0 Author: Yan Yablonovskiy <[email protected]> Date: Sat Nov 22 13:48:50 2025 +1100 Merge branch 'leanprover-community:master' into master commit 6534400 Merge: bb1a642 56c98a5 Author: Yan Yablonovskiy <[email protected]> Date: Thu Nov 20 18:46:50 2025 +1100 Merge branch 'leanprover-community:master' into master commit bb1a642 Author: YanYablonovskiy <[email protected]> Date: Mon Oct 20 21:27:21 2025 +1100 Update OrderType.lean commit f427a91 Author: YanYablonovskiy <[email protected]> Date: Mon Oct 20 18:25:16 2025 +1100 Update OrderType.lean commit f6c13a0 Author: YanYablonovskiy <[email protected]> Date: Mon Oct 20 17:59:56 2025 +1100 Update OrderType.lean commit 78e4c9a Author: YanYablonovskiy <[email protected]> Date: Mon Oct 20 16:29:31 2025 +1100 Update OrderType.lean commit e827b3c Author: YanYablonovskiy <[email protected]> Date: Sat Oct 18 00:41:45 2025 +1100 Update OrderType.lean commit f5d5427 Author: YanYablonovskiy <[email protected]> Date: Sat Oct 18 00:23:18 2025 +1100 Update OrderType.lean commit 871acb9 Author: YanYablonovskiy <[email protected]> Date: Fri Oct 17 22:32:05 2025 +1100 Update OrderType.lean commit 803ced6 Author: YanYablonovskiy <[email protected]> Date: Fri Oct 17 20:45:37 2025 +1100 Update OrderType.lean commit 2883e90 Author: YanYablonovskiy <[email protected]> Date: Thu Oct 16 23:04:21 2025 +1100 Update OrderType.lean commit 971c382 Author: Yan Yablonovskiy <[email protected]> Date: Thu Oct 16 23:02:18 2025 +1100 Update OrderType.lean commit 3db4465 Author: Yan Yablonovskiy <[email protected]> Date: Thu Oct 16 23:01:46 2025 +1100 Update OrderType.lean commit 3e7c325 Author: YanYablonovskiy <[email protected]> Date: Thu Oct 16 22:59:05 2025 +1100 Update OrderType.lean commit ce284fa Author: Yan Yablonovskiy <[email protected]> Date: Tue Oct 14 20:26:41 2025 +1100 Update OrderType.lean commit e0e79c8 Author: YanYablonovskiy <[email protected]> Date: Tue Oct 14 19:02:32 2025 +1100 Create OrderTypes file with definition and some generalisation from Ordinal commit e78fa58 Merge: aa54d18 3aa3aca Author: Yan Yablonovskiy <[email protected]> Date: Tue Oct 14 19:02:04 2025 +1100 Merge branch 'leanprover-community:master' into master commit aa54d18 Merge: 3742a3b efcc0aa Author: Yan Yablonovskiy <[email protected]> Date: Sun Sep 21 15:21:45 2025 +1000 Merge branch 'leanprover-community:master' into master commit 3742a3b Author: YanYablonovskiy <[email protected]> Date: Sat Sep 20 22:28:23 2025 +1000 Create OrderTypes_basic.lean

Co-authored-by: Violeta Hernández Palacios <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>

Add copyright [skip actions]

[skip ci] Co-authored-by: Yaël Dillies <[email protected]> Co-authored-by: Violeta Hernández Palacios <[email protected]>

Co-authored-by: Yaël Dillies <[email protected]> Co-authored-by: Violeta Hernández Palacios <[email protected]>

`OrderType.lean` no longer exists

Co-authored-by: Violeta Hernández Palacios <[email protected]>

mathlib4-dependent-issues-bot · 2026-01-17T07:22:48Z

This PR/issue depends on:

feat(Order): order types #34034
By Dependent Issues (🤖). Happy coding!

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Dec 31, 2025

github-actions bot added the t-order Order theory label Dec 31, 2025

vihdzp reviewed Dec 31, 2025

View reviewed changes

YaelDillies reviewed Dec 31, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 31, 2025

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 4, 2026

YaelDillies reviewed Jan 4, 2026

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 4, 2026

vihdzp reviewed Jan 4, 2026

View reviewed changes

Mathlib/Order/Hom/Basic.lean Outdated Show resolved Hide resolved

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 5, 2026

vihdzp reviewed Jan 5, 2026

View reviewed changes

YaelDillies changed the title ~~feat: OrderTypes~~ feat: order types Jan 5, 2026

YanYablonovskiy mentioned this pull request Jan 6, 2026

[Merged by Bors] - feat(Order): OrderIso involving Prod and Lex #33663

Closed

YanYablonovskiy force-pushed the master branch from 4c41035 to d6fa0fb Compare January 6, 2026 10:27

YanYablonovskiy force-pushed the master branch from d4daec0 to 6e9cfd2 Compare January 6, 2026 11:28

YanYablonovskiy and others added 23 commits January 16, 2026 15:53

Update OrderType.lean

5c7eecb

Update OrderType.lean

c64b512

Update OrderType.lean

fb0b868

Update OrderType.lean

2626f35

Update OrderType.lean

3ffda1d

Apply suggestions from code review

179c5c1

Co-authored-by: Violeta Hernández Palacios <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>

Update OrderType.lean

58f6b09

Update OrderType.lean

580ecfb

Add copyright [skip actions]

Clean up imports, get rid of sorries, and address some comments

6bc98e1

Bump

dae7f9e

Fix module error

83154e2

Style fix

88cf3f0

Apply suggestions from code review

2e88771

[skip ci] Co-authored-by: Yaël Dillies <[email protected]> Co-authored-by: Violeta Hernández Palacios <[email protected]>

Finish conversation review suggestions

b215430

Minor typos

e27e412

Add doc-string and some more typos

c9d8216

Fix recommended_spellings

9886505

Apply suggestions from code review

3970088

Co-authored-by: Yaël Dillies <[email protected]> Co-authored-by: Violeta Hernández Palacios <[email protected]>

Apply suggestions

6468ea9

Refactor as per suggestions, back to LinOrd

b235289

Change mathlib imports from OrderType

d1a7d79

`OrderType.lean` no longer exists

Apply suggestions from code review

d47b8cf

Co-authored-by: Violeta Hernández Palacios <[email protected]>

Changes from review

3e07307

YanYablonovskiy force-pushed the master branch from 6e9cfd2 to 3e07307 Compare January 16, 2026 04:54

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 16, 2026

Apply suggestion 0 < o → o ≠ 0 to 0 < o ↔ o ≠ 0

9c47226

YanYablonovskiy mentioned this pull request Jan 16, 2026

feat(Order): order types #34034

Open

2 tasks

YaelDillies changed the title ~~feat: order types~~ feat: more API about order types Jan 17, 2026

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 17, 2026

	instance instNeZeroOne : NeZero (1 : OrderType) :=
	instance : NeZero (1 : OrderType) :=

feat: more API about order types #33420

Are you sure you want to change the base?

feat: more API about order types #33420

Conversation

YanYablonovskiy commented Dec 31, 2025 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary b79634a5c1

Import changes for modified files

Declarations diff

Uh oh!

vihdzp left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

vihdzp left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

YaelDillies Dec 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

vihdzp commented Jan 1, 2026

Uh oh!

YanYablonovskiy commented Jan 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YanYablonovskiy commented Jan 4, 2026

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

vihdzp Jan 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YanYablonovskiy commented Dec 31, 2025 •

edited by YaelDillies

Loading

github-actions bot commented Dec 31, 2025 •

edited

Loading

YaelDillies Dec 31, 2025 •

edited

Loading

YanYablonovskiy commented Jan 4, 2026 •

edited

Loading

vihdzp Jan 4, 2026 •

edited

Loading

vihdzp commented Jan 4, 2026 •

edited

Loading

vihdzp Jan 5, 2026 •

edited

Loading