Environment の書き換えを使って、一度定義した変数の値を書き換えられるか？

できますが、公開 API だけでは不可です。Environment のコンストラクタや同期更新関数は private で、公式実装にも「環境は破壊的更新されない」「定数マップはカーネルで型検査済みの宣言を保持する」と明記されています。 

実験目的なら、unsafeCast で private 実装を回避する「壊すコード」は書けます。

import Lean
open Lean Elab Command
namespace RewriteDefUnsafe
/--
危険版：def の本体を Environment 内で差し替える。
注意：

• soundness を壊す。
• Lean のバージョン差分で壊れる可能性が高い。
• .olean 出力や async elaboration との整合性も保証しない。
• 学習・実験用。
  -/
  unsafe def replaceDefValueUnsafe
  (env : Environment) (declName : Name) (newValue : Expr) :
  Except String Environment := do
  let kenv := env.toKernelEnv
  let some cinfo := kenv.find? declName
  | throw s!"unknown declaration: {declName}"
  let newCInfo ←
  match cinfo with
  | .defnInfo v =>
  pure <| ConstantInfo.defnInfo { v with value := newValue }
  | _ =>
  throw s!"not a definition: {declName}"
  let newKEnv : Kernel.Environment :=
  { kenv with
  constants := kenv.constants.insert declName newCInfo }
  -- Environment.ofKernelEnv は kernel env から elaborator env を作る公開関数。
  -- 既存の elaboration state の細部は捨てるので、実験用。
  pure <| Environment.ofKernelEnv newKEnv
  unsafe def replaceCurrentDefValueUnsafe
  (declName : Name) (newValue : Expr) : CommandElabM Unit := do
  let env ← getEnv
  match replaceDefValueUnsafe env declName newValue with
  | .ok env' => setEnv env'
  | .error e => throwError e
  syntax "#replace_nat_def " ident " := " num : command
  unsafe elab_rules : command
  | `(#replace_nat_def $x:ident := $n:num) => do
  -- Nat リテラルの Expr を作る
  let newValue := mkNatLit n.getNat
  replaceCurrentDefValueUnsafe x.getId newValue
  end RewriteDefUnsafe

使用例：

import Lean
open RewriteDefUnsafe
def x : Nat := 1
#eval x
-- 1
#replace_nat_def x := 42
#eval x
-- 42 になる可能性がある

ただし、これは Lean の正規機能ではなく、Environment の不変条件を破壊する実験です。addDeclCore は宣言を追加して elaborator 側の async constant map も更新しますが、上のコードはそこを正しく再現していません。公式実装でも addDeclCore はカーネル環境と elaborator 側マップを同期させています。 

Start by reading the Environment constructor, synchronization update functions, and addDeclCore referenced in the issue, focusing on how the kernel environment and elaborator-side async constant map stay synchronized. Clarify whether the intended outcome is documentation or a maintained experiment; done should state the supported limitation and the risks of the unsafe replacement approach.