From c334bf978434a789ff9411b2575e915221cdd6e6 Mon Sep 17 00:00:00 2001
From: Maximus Gorog <mgorog@gmail.com>
Date: Wed, 6 May 2026 01:43:00 -0600
Subject: [PATCH] =?UTF-8?q?Remove=20Test/Reify.lean=20=E2=80=94=20Phase=20?=
 =?UTF-8?q?1=20macro-debugging=20scratch?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The Phase 1 agent left a 42-line scratch file (myDeriveDimVar15
suggests attempt #15) from the macro-iteration cycle.  Not in the
root barrel; not exercised by tests; pure dead code.

Per the "no parallel dead-code definitions" discipline.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 CubicalTransport/Test/Reify.lean | 42 --------------------------------
 1 file changed, 42 deletions(-)
 delete mode 100644 CubicalTransport/Test/Reify.lean

diff --git a/CubicalTransport/Test/Reify.lean b/CubicalTransport/Test/Reify.lean
deleted file mode 100644
index 81f0559..0000000
--- a/CubicalTransport/Test/Reify.lean
+++ /dev/null
@@ -1,42 +0,0 @@
-import Lean
-import CubicalTransport.Syntax
-namespace CubicalTransport.Test.Reify
-
-partial def reifyStrLit (e : Lean.Expr) : Lean.MetaM (Option String) := do
-  let e ← Lean.Meta.whnf e
-  match e with
-  | .lit (.strVal s) => return some s
-  | _ => return none
-
-open Lean Elab Command Term Lean.Parser.Term
-
-elab "myDeriveDimVar15" : command => do
-  let lExpr := mkCIdent ``Lean.Expr
-  let lMetaM := mkCIdent ``Lean.MetaM
-  let lOption := mkCIdent ``Option
-  let lDimVar := mkCIdent ``DimVar
-  let lWhnf := mkCIdent ``Lean.Meta.whnf
-  let lDimVarMk := mkCIdent ``DimVar.mk
-  let lReifyStrLit := mkCIdent `CubicalTransport.Test.Reify.reifyStrLit
-  let arm1Body : TSyntax ``Lean.Parser.Term.doSeq ←
-    `(doSeq| if h : args.size = 1 then
-                match ← ($lReifyStrLit (args[0]'(by omega))) with
-                | none => return none
-                | some name_ => return some (@$lDimVarMk name_)
-             else
-                return none)
-  let pat1 ← `(($(quote ``DimVar.mk), args))
-  let pat2 ← `(_)
-  let body2 ← `(doSeq| return none)
-  let pats : Array Term := #[pat1, pat2]
-  let bodies : Array (TSyntax ``Lean.Parser.Term.doSeq) := #[arm1Body, body2]
-  -- Splice (pat, body) pairs:
-  let cmd ← `(partial def reifyDimVar' : $lExpr → $lMetaM ($lOption $lDimVar) := fun e => do
-                let e ← ($lWhnf e)
-                match (e).getAppFnArgs with
-                $[| $pats => $bodies]*)
-  elabCommand cmd
-
-myDeriveDimVar15
-
-end CubicalTransport.Test.Reify