Remove Module.liftR' and Module.liftL' as well

VCA-EPFL · Oct 29, 2024 · b9eb39a · b9eb39a
1 parent dd01af2
commit b9eb39a
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/DataflowRewriter/Examples/BranchMerge.lean b/DataflowRewriter/Examples/BranchMerge.lean
@@ -109,6 +109,8 @@ def test4 (TagT T S : Type) [h:DecidableEq TagT] (input output : (T : Type) × (
     -- conv in _ :: Module.connect'' _ _ :: _ => arg 2; arg 2; rw [Module.connect''_dep_rw]; rfl
     unfold Module.connect''
     dsimp
+    unfold Module.liftR' Module.liftL'
+    dsimp
 
 end BranchMerge