module Chapter5.IDesc.Examples.Walk where open import Level hiding (suc) renaming (zero to zeroL) open import Data.Unit open import Data.Nat open import Data.Fin hiding (lift) open import Data.Vec open import Data.Product open import Relation.Binary.PropositionalEquality open import Chapter5.IDesc open import Chapter5.IDesc.Fixpoint open import Chapter5.IDesc.Tagged WalkD : tagDesc zeroL ℕ WalkD = (1 , (λ n → `var (suc n) `× `1 ∷ [])) , ((λ { zero → 1 ; (suc n) → 1 }) , λ { zero → `1 ∷ [] ; (suc n) → `var n `× `1 ∷ [] }) Walk : ℕ → Set Walk = μ (toDesc WalkD) up : ∀{n} → Walk (suc n) → Walk n up w = ⟨ lift zero , w , lift tt ⟩ stop : Walk 0 stop = ⟨ lift (suc zero) , lift tt ⟩ down : ∀{n} → Walk n → Walk (suc n) down w = ⟨ lift (suc zero) , w , lift tt ⟩