module FunOrn.FunOrnament.Examples.Lookup where

open import Data.Unit

open import Logic.Logic

open import IDesc.Examples.Nat

open import Orn.Ornament
open import Orn.Ornament.Identity
open import Orn.Ornament.Examples.List
open import Orn.Ornament.Examples.Maybe

open import FunOrn.Functions.Examples.Le

open import FunOrn.FunOrnament

-- Paper: Example 5.8
typeLookup : (A : Set)  FunctionOrn type<
typeLookup A = μ⁺ idO NatD [ inv tt ]→ 
               μ⁺ ListO A [ inv tt ]→ 
               μ⁺ MaybeO A [ inv tt  `⊤