max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: Add a docstring to Simp.Result and its fields (#3319)

Browse source
This commit is contained in:
Eric Wieser 2024-02-13 13:57:24 +00:00 • committed by GitHub
parent 3a6ebd88bb
commit 0554ab39aa
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Meta/Tactic/Simp/Types.lean
View file

@ -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. -/