diff --git a/Language.agda b/Language.agda index d9d25e2..4b37771 100644 --- a/Language.agda +++ b/Language.agda @@ -3,7 +3,7 @@ module Language where open import Data.Nat using (ℕ; suc; pred) open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.Product using (Σ; _,_; proj₁; proj₂) -open import Data.Vec using (Vec; foldr) +open import Data.Vec using (Vec; foldr; lookup) open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ) open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_) @@ -83,6 +83,9 @@ record Program : Set where State : Set State = Fin length + code : State → Stmt + code = lookup stmts + states : List State states = proj₁ (indices length)