chore: add doc-string for Prod.mk
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 979bf82..197b3e2 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean
@@ -477,6 +477,8 @@ For more information: [Constructors with Arguments](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html?highlight=Prod#constructors-with-arguments) -/ structure Prod (α : Type u) (β : Type v) where + /-- Constructs a pair from two terms. -/ + mk :: /-- The first projection out of a pair. if `p : α × β` then `p.1 : α`. -/ fst : α /-- The second projection out of a pair. if `p : α × β` then `p.2 : β`. -/