Skip to content

Commit

Permalink
Indicate implicit argument in lambda pattern
Browse files Browse the repository at this point in the history
  • Loading branch information
jacquescomeaux committed Aug 9, 2024
1 parent de29737 commit f25b6e7
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record
}
; p₁∘universal≈h₁ = X.refl
; p₂∘universal≈h₂ = Y.refl
; unique-diagram = λ eq₁ eq₂ eq₁ , eq₂
; unique-diagram = λ eq₁ eq₂ {_} eq₁ , eq₂
}
}
where
Expand Down

0 comments on commit f25b6e7

Please sign in to comment.