From 0554ab39aaa56473fe0a0076f1d758fde3f08fe9 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 13 Feb 2024 13:57:24 +0000
Subject: [PATCH] doc: Add a docstring to `Simp.Result` and its fields (#3319)

---
 src/Lean/Meta/Tactic/Simp/Types.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 978218efc1..7d3da91d0f 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -12,9 +12,13 @@ import Lean.Meta.Tactic.Simp.SimpCongrTheorems
 namespace Lean.Meta
 namespace Simp
 
+/-- The result of simplifying some expression `e`. -/
 structure Result where
+  /-- The simplified version of `e` -/ 
   expr           : Expr
-  proof?         : Option Expr := none -- If none, proof is assumed to be `refl`
+  /-- A proof that `$e = $expr`, where the simplified expression is on the RHS.
+  If `none`, the proof is assumed to be `refl`. -/
+  proof?         : Option Expr := none
   /-- Save the field `dischargeDepth` at `Simp.Context` because it impacts the simplifier result. -/
   dischargeDepth : UInt32 := 0
   /-- If `cache := true` the result is cached. -/