module Chapter8.Ornament.Examples.Fin where open import Level hiding (zero ; suc) open import Function open import Data.Empty open import Data.Unit open import Data.Nat open import Data.Fin hiding (lift) open import Data.Product open import Relation.Binary.PropositionalEquality open import Chapter2.Logic open import Chapter5.IDesc open import Chapter5.IDesc.Fixpoint open import Chapter5.IDesc.Examples.Nat open import Chapter8.Ornament u : ℕ → ⊤ u _ = tt module Constraint where FinO : orn NatD u u FinO = orn.mk λ n → `σ (λ { zero → insert ℕ λ m → insert (suc m ≡ n) λ _ → `1 ; (suc zero) → insert ℕ λ m → insert (suc m ≡ n) λ _ → `var (inv m) `× `1 ; (suc (suc ())) }) Fin' : ℕ → Set Fin' = μ ⟦ FinO ⟧orn fz : ∀{n} → Fin' (suc n) fz {n} = ⟨ zero , n , refl , lift tt ⟩ fs : ∀{n} → Fin' n → Fin' (suc n) fs {n} k = ⟨ suc zero , n , refl , k , lift tt ⟩ module Compute where FinO : orn NatD u u FinO = orn.mk λ { zero → insert ⊥ ⊥-elim ; (suc n) → `σ λ { zero → `1 ; (suc zero) → `var (inv n) `× `1 ; (suc (suc ())) } } Fin' : ℕ → Set Fin' = μ ⟦ FinO ⟧orn fz : ∀{n} → Fin' (suc n) fz {n} = ⟨ zero , lift tt ⟩ fs : ∀{n} → Fin' n → Fin' (suc n) fs {n} k = ⟨ suc zero , k , lift tt ⟩