chore: make section names more meaningful

leanprover · Oct 4, 2024 · fa4030e · fa4030e
1 parent 366d482
commit fa4030e
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/Tactics/Sym/AxEffects.lean b/Tactics/Sym/AxEffects.lean
@@ -88,9 +88,9 @@ structure AxEffects where
 
 namespace AxEffects
 
-/-! ## Monad getters -/
+/-! ## Monadic getters -/
 
-section Monad
+section MonadicGetters
 variable {m} [Monad m] [MonadReaderOf AxEffects m]
 
 def getCurrentState       : m Expr := do return (← read).currentState
@@ -117,7 +117,7 @@ def getCurrentStateName : m Name := do
       | throwError "error: unknown fvar: {state}"
     return decl.userName
 
-end Monad
+end MonadicGetters
 
 /-! ## Initial Reflected State -/
 
@@ -236,7 +236,7 @@ def getField (eff : AxEffects) (fld : StateField) : MetaM FieldEffect :=
       let proof  ← eff.mkAppNonEffect (toExpr fld)
       pure { value, proof }
 
-section Monad
+section MonadicGettersAndSetters
 variable {m} [Monad m] [MonadLiftT MetaM m]
 
 variable [MonadReaderOf AxEffects m] in
@@ -264,7 +264,7 @@ This is a specialization of `setFieldEffect`. -/
 def setErrorProof (proof : Expr) : m Unit :=
   setFieldEffect .ERR { value := mkConst ``StateError.None, proof }
 
-end Monad
+end MonadicGettersAndSetters
 
 /-! ## Update a Reflected State -/
 

diff --git a/Tactics/Sym/Context.lean b/Tactics/Sym/Context.lean
@@ -169,7 +169,7 @@ or throw an error if no local variable of that name exists -/
 def hRunDecl : MetaM LocalDecl := do
   findFromUserName c.h_run
 
-section Monad
+section MonadicGetters
 variable {m} [Monad m] [MonadReaderOf SymContext m]
 
 def getCurrentStateNumber : m Nat := do return (← read).currentStateNumber
@@ -187,7 +187,7 @@ def getNextStateName : m Name := do
   let c ← read
   return Name.mkSimple s!"{c.state_prefix}{c.currentStateNumber + 1}"
 
-end Monad
+end MonadicGetters
 
 end