Also modify example in Merge

VCA-EPFL · Oct 29, 2024 · f200cbf · f200cbf
1 parent 71668ab
commit f200cbf
Showing 1 changed file with 1 addition and 9 deletions.
diff --git a/DataflowRewriter/Examples/Merge.lean b/DataflowRewriter/Examples/Merge.lean
@@ -16,6 +16,7 @@ import DataflowRewriter.KernelRefl
 import DataflowRewriter.Reduce
 import DataflowRewriter.List
 import DataflowRewriter.ExprHighLemmas
+import DataflowRewriter.Tactic
 
 open Batteries (AssocList)
 
@@ -26,15 +27,6 @@ namespace DataflowRewriter
 
 abbrev Ident := Nat
 
-elab "precompute " t:term : tactic => Tactic.withMainContext do
-  let expr ← Term.elabTerm t none
-  Term.synthesizeSyntheticMVarsUsingDefault
-  let expr ← Lean.instantiateMVars expr
-  let expr ←
-    -- withTransparency .all <|
-      reallyReduce (skipArgs := false) (skipTypes := false) expr
-  (← Tactic.getMainGoal).assign expr
-
 def threemerge T : NatModule (List T):=
   { inputs := [(0, ⟨ T, λ oldList newElement newList => newList = newElement :: oldList ⟩),
                (1, ⟨ T, λ oldList newElement newList => newList = newElement :: oldList ⟩),