diff --git a/src/Data/Wedge.agda b/src/Data/Wedge.agda index 1e076ca..c96a0f9 100644 --- a/src/Data/Wedge.agda +++ b/src/Data/Wedge.agda @@ -100,10 +100,11 @@ swap (there b) = here b -- Wedge associativity reassocLR : Wedge (Wedge A B) C -> Wedge A (Wedge B C) -reassocLR (here (here a)) = here a -reassocLR (here (there b)) = there (here b) reassocLR (there c) = there (there c) -reassocLR _ = nowhere +reassocLR (here (there b)) = there (here b) +reassocLR (here (here a)) = here a +reassocLR (here nowhere) = nowhere +reassocLR nowhere = nowhere reassocRL : Wedge A (Wedge B C) -> Wedge (Wedge A B) C reassocRL nowhere = nowhere @@ -112,8 +113,6 @@ reassocRL (there nowhere) = nowhere reassocRL (there (here b)) = here (there b) reassocRL (there (there c)) = there c --- - -- conversions fromSum : A + B -> Wedge A B @@ -126,8 +125,6 @@ quotWedge (left nothing) = nowhere quotWedge (right (just b)) = there b quotWedge (right nothing) = nowhere --- 1 + (A + B) <=> Wedge A B - -- collapses both nothing into single nowhere toWedge : Maybe (A + B) -> Wedge A B toWedge (just (left a)) = here a @@ -141,12 +138,10 @@ fromWedge (there b) = just (right b) -- projections --- TODO fromHere (quotWedge Nothing mb) = mb fromHere : Wedge A B -> Maybe A fromHere (here a) = just a fromHere _ = nothing --- TODO fromThere (quotWedge ma Nothing) = ma fromThere : Wedge A B -> Maybe B fromThere (there b) = just b fromThere _ = nothing