sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

style: format

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-04 09:50:15 -03:00
parent af12f7e9be
commit a7aea9a12d
1 changed files with 6 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
src/Std/Internal/Http/Data/Extensions.lean
View File

@@ -38,15 +38,15 @@ protected def Extensions.compareName : Name → Name → Ordering
| .anonymous, _ => .lt
| _, .anonymous => .gt
| .str p₁ s₁, .str p₂ s₂ =>
match Extensions.compareName p₁ p₂ with
| .eq => compareOfLessAndEq s₁ s₂
| ord => ord
match Extensions.compareName p₁ p₂ with
| .eq => compareOfLessAndEq s₁ s₂
| ord => ord
| .str _ _, .num _ _ => .lt
| .num _ _, .str _ _ => .gt
| .num p₁ n₁, .num p₂ n₂ =>
match Extensions.compareName p₁ p₂ with
| .eq => compare n₁ n₂
| ord => ord
match Extensions.compareName p₁ p₂ with
| .eq => compare n₁ n₂
| ord => ord
/--
A dynamically typed map for optional metadata that can be attached to HTTP requests and responses.