module FunOrn.FunOrnament.Examples.Append where

open import Data.Unit

open import Logic.Logic

open import IDesc.Examples.Nat

open import Orn.Ornament
open import Orn.Ornament.Examples.List

open import FunOrn.Functions.Examples.Plus

open import FunOrn.FunOrnament

-- Paper: Example 5.10
typeAppend : (A : Set)  FunctionOrn type+
typeAppend A = μ⁺ ListO A [ inv tt ]→ 
               μ⁺ ListO A [ inv tt ]→ 
               μ⁺ ListO A [ inv tt  `⊤