We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 4bc1084 commit c774612Copy full SHA for c774612
1 file changed
src/Vatras/Lang/ADT/Merge.agda
@@ -23,9 +23,9 @@ module Named (F : 𝔽) where
23
This operations inherits all properties of the variant composition (e.g., commutativity, associativity etc).
24
-}
25
_⊕_ : ∀ {A} → ADT A → ADT A → ADT A
26
- leaf l ⊕ leaf r = leaf (l +ᵥ r)
27
- leaf l ⊕ (E ⟨ el , er ⟩) = E ⟨ leaf l ⊕ el , leaf l ⊕ er ⟩
28
- (D ⟨ dl , dr ⟩) ⊕ r = D ⟨ dl ⊕ r , dr ⊕ r ⟩
+ leaf l ⊕ leaf r = leaf (l +ᵥ r)
+ leaf l ⊕ (E ⟨ el , er ⟩) = E ⟨ leaf l ⊕ el , leaf l ⊕ er ⟩
+ (D ⟨ dl , dr ⟩) ⊕ r = D ⟨ dl ⊕ r , dr ⊕ r ⟩
29
30
⊕-spec : ∀ {A} (l r : ADT A) (c : Configuration) →
31
⟦ l ⊕ r ⟧ c ≡ ⟦ l ⟧ c +ᵥ ⟦ r ⟧ c
0 commit comments