module Chapter9.Functions.Examples.Plus where open import Level renaming ( zero to zeroL ; suc to sucL ) open import Data.Unit open import Data.Fin hiding (_+_ ; lift) open import Data.Product open import Chapter5.IDesc open import Chapter5.IDesc.Fixpoint open import Chapter5.IDesc.Induction open import Chapter5.IDesc.Examples.Nat hiding (ze ; su) open import Chapter9.Functions type+ : Type zeroL type+ = μ NatD [ tt ]→ μ NatD [ tt ]→ μ NatD [ tt ]× `⊤ infix 40 _+_ pattern ze = ⟨ zero , lift tt ⟩ pattern su n = ⟨ suc zero , n , lift tt ⟩ _+'_ : ⟦ type+ ⟧Type m +' ze = m , lift tt m +' su n = su (proj₁ (m +' n)) , lift tt m +' ⟨ suc (suc ()) , _ ⟩ α : Nat → DAlg NatD (λ _ → Nat × Lift ⊤) α m {tt} {zero , lift tt} (lift tt) = m , lift tt α m {tt} {suc zero , n , lift tt} ((m+n , lift tt) , lift tt) = su m+n , lift tt α m {tt} {suc (suc ()) , _} _ _+_ : ⟦ type+ ⟧Type m + n = induction NatD (λ _ → Nat × Lift ⊤) (λ {i}{xs} → α m {i}{xs}) n private module Test where open import Relation.Binary.PropositionalEquality test-0+0 : ze + ze ≡ ze +' ze test-0+0 = refl test-m+0 : ∀{m} → m + ze ≡ (m , lift tt) test-m+0 = refl test-m+1 : ∀{m} → m + (su ze) ≡ m +' (su ze) test-m+1 = refl test-m+2 : ∀{m} → m + (su (su ze)) ≡ m +' (su (su ze)) test-m+2 = refl