Remove Test/Reify.lean — Phase 1 macro-debugging scratch
Some checks are pending
Lean Action CI / build (push) Waiting to run

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>
This commit is contained in:
Maximus Gorog 2026-05-06 01:43:00 -06:00
parent 2417ec667b
commit c334bf9784

View file

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