diff --git a/Language.agda b/Language.agda index 7ece4ea..de86158 100644 --- a/Language.agda +++ b/Language.agda @@ -352,7 +352,7 @@ module Graphs where buildCfg (while _ repeat s) = (buildCfg s ⟨⊗⟩ pushEmptyBlock ⟨⊗⟩ pushEmptyBlock) update (λ { g ((idx₁ , idx₂) , idx , idx') → - addEdges g ((idx , idx') ∷ (idx₂ , idx) ∷ []) }) + addEdges g ((idx , idx') ∷ (idx , idx₁) ∷ (idx₂ , idx) ∷ []) }) map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') }) open import Lattice.MapSet _≟ˢ_