From 791d3447737e94fda2f2f9be7c760fdd29250f5d Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Sat, 31 Aug 2024 01:05:46 +0200
Subject: [PATCH] doc string for LSimp.Result and MetaMCtxM

---
 SciLean/Tactic/GTrans/MetaLCtxM.lean | 23 +++++++++++++++++++++++
 SciLean/Tactic/LSimp/Types.lean      | 12 ++++++++++++
 2 files changed, 35 insertions(+)

diff --git a/SciLean/Tactic/GTrans/MetaLCtxM.lean b/SciLean/Tactic/GTrans/MetaLCtxM.lean
index f0c9a661..0599e117 100644
--- a/SciLean/Tactic/GTrans/MetaLCtxM.lean
+++ b/SciLean/Tactic/GTrans/MetaLCtxM.lean
@@ -38,6 +38,29 @@ def _root_.Lean.Meta.Context.mkCtxCfg (ctx : ContextCtx) (cfg : ContextCfg) : Me
 
 -- TODO: change the monad such that we can only add variables to the context and not remove them
 --       or completely changes the context
+/-- Similar to `MetaM` but allows modifying local context.
+
+Most imporantly it has a variant of `lambdaTelescope` called `introLet` such that instead of
+```
+lambdaTelescope e fun xs b => do
+  f xs b
+```
+we can call
+```
+let (b,xs) ← lambdaIntro e
+f xs b
+```
+
+For example running `lambdaTelescope` does not work well with for loops but `lambdaIntro` does.
+
+Important functions introducing new free variables to the context:
+  - `lambdaIntro`
+  - `letIntro`
+  - `introLocalDecl`
+  - `introLetDecl`
+
+Also you can run `MetaLCtxM` inside of `MetaM` with `MetaLCtxM.runInMeta`.
+ -/
 abbrev MetaLCtxM  := ReaderT Meta.ContextCfg $ StateT Meta.ContextCtx $ StateRefT Meta.State CoreM
 
 
diff --git a/SciLean/Tactic/LSimp/Types.lean b/SciLean/Tactic/LSimp/Types.lean
index e866bd9a..a055c1fc 100644
--- a/SciLean/Tactic/LSimp/Types.lean
+++ b/SciLean/Tactic/LSimp/Types.lean
@@ -20,9 +20,21 @@ namespace SciLean.Tactic.LSimp
 -- Result ------------------------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------------
 
+
+/-- Result of `lsimp` -/
 structure Result where
+  /-- Result of simplification  -/
   expr : Expr
+  /-- Proof that the result is propositionally equal to the original expression. It is `none` if
+  it is defeq to the original. -/
   proof? : Option Expr := none
+  /-- This array keeps track of the newly introduced free variables that appear in the result.
+  We run `lsimp` in `MetaLCtxM` which allows modifying the local context by adding new free
+  variables.
+
+  See `Result.bindVars` which is a function that takes the result and the proof and binds all
+  these newly introduced free variables such that the result is valid in the original context
+  of the expression we are simplifying. -/
   vars : Array Expr := #[]
   cache          : Bool := true
   deriving Inhabited