Cleanup another definition

VCA-EPFL · Oct 24, 2024 · 841e35b · 841e35b
1 parent ffdaa1b
commit 841e35b
Showing 1 changed file with 0 additions and 7 deletions.
diff --git a/DataflowRewriter/Examples/BranchMerge.lean b/DataflowRewriter/Examples/BranchMerge.lean
@@ -72,13 +72,6 @@ example y : (fun S TagT T input output internals =>
   conv in _ :: Module.connect'' _ _ :: _ => arg 2; rw [connect_r]; rfl
   sorry
 
-example y : (fun f : Nat → Nat => ∀ (wf : Nat = Nat), ∃ b, (match ({ a := "", b := "b" } : A) == { a := "", b := "c" } with
-             | true => wf.mp 1
-             | false => wf.mpr 2) = f b) y := by
-  -- simp
-  simp [BEq.beq]
-  sorry
-
 @[drunfold]
 def tagged_ooo_h : ExprHigh String :=
 [graph|