refined WalkingshawVariant to reuse Artifacts

VariantSync · Nov 3, 2023 · d21751a · d21751a
1 parent 19a2610
commit d21751a
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/Framework/V2/Variants.agda b/src/Framework/V2/Variants.agda
@@ -9,16 +9,16 @@ open import Relation.Binary using (Setoid)
 import Relation.Binary.PropositionalEquality as Eq
 
 open import Framework.V2.Definitions using (𝕍; 𝔸)
+open import Framework.V2.Constructs.Artifact using (Artifact)
 
 import Data.IndexedSet
 
 data GrulerVariant : 𝕍 where
   asset : ∀ {A : 𝔸} (a : A) → GrulerVariant A
   _∥_   : ∀ {A : 𝔸} (l : GrulerVariant A) → (r : GrulerVariant A) → GrulerVariant A
 
-data WalkingshawVariant : 𝕍 where
-  -- TODO: Use Artifact Construct here.
-  _-<_>- : ∀ {A : 𝔸} (a : A) → List (WalkingshawVariant A) → WalkingshawVariant A
+data Rose : 𝕍 where
+  artifact : ∀ {A : 𝔸} → Artifact A (Rose A) → Rose A
 
 VariantSetoid : 𝕍 → 𝔸 → Setoid 0ℓ 0ℓ
 VariantSetoid V A = Eq.setoid (V A)