module Chapter5.IDesc.Examples.Fin where open import Level renaming ( zero to zeroL ; suc to sucL ) open import Data.Unit open import Data.Nat open import Data.Fin hiding (lift) renaming (Fin to FinNative) 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 module Compute where FinD : tagDesc zeroL ℕ FinD = (0 , λ n → []) , ((λ { zero → 0 ; (suc n) → 2 }) , λ { zero → [] ; (suc n) → `1 ∷ `var n `× `1 ∷ []}) Fin : ℕ → Set Fin = μ (toDesc FinD) ze : ∀{n} → Fin (suc n) ze = ⟨ lift zero , lift tt ⟩ su : ∀{n} → Fin n → Fin (suc n) su k = ⟨ lift (suc zero) , k , lift tt ⟩ module Constraint where FinD : tagDesc zeroL ℕ FinD = (2 , λ n → (`Σ ℕ λ m → `Σ (n ≡ suc m) λ _ → `1) ∷ (`Σ ℕ λ m → `Σ (n ≡ suc m) λ _ → `var m `× `1) ∷ []) , (λ n → 0) , λ n → [] Fin : ℕ → Set Fin = μ (toDesc FinD) ze : ∀{n} → Fin (suc n) ze = ⟨ lift zero , _ , refl , lift tt ⟩ su : ∀{n} → Fin n → Fin (suc n) su k = ⟨ lift (suc zero) , _ , refl , k , lift tt ⟩