Skip to content

Commit e4b9434

Browse files
williamdemeoclaude
andcommitted
Name the map argument in cores-range-⊆'s clause head
Address a review nit: the clause head now mirrors the type signature. `m` is unused in the body (the proof only inspects the membership proof), but naming it saves the reader a trip to the signature to recover the argument order. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
1 parent b42be08 commit e4b9434

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

  • src-lib-exts/abstract-set-theory/Axiom/Set/Map

src-lib-exts/abstract-set-theory/Axiom/Set/Map/Extra.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -711,7 +711,7 @@ module _ {A B : Type}
711711
-- The map `m` is an explicit argument because it cannot be recovered by unification:
712712
-- `_∣^_` goes through `⊆-map`, which mentions `m` only as `m ˢ` (i.e., `proj₁ m`).
713713
cores-range-⊆ : {A B : Type} ⦃ _ : DecEq B ⦄ (m : A ⇀ B) {X : ℙ B} range (m ∣^ X) ⊆ X
714-
cores-range-⊆ _ b∈range with Equivalence.from ∈-map b∈range
714+
cores-range-⊆ m b∈range with Equivalence.from ∈-map b∈range
715715
... | _ , refl , ab∈cores = proj₁ (Equivalence.from ∈-filter ab∈cores)
716716

717717

0 commit comments

Comments
 (0)