datatype id = n_1 | n_2

type_synonym entry = "(id * (entry list ⇒ nat))"
type_synonym myList = "entry list"

fun ivalue :: "myList ⇒ nat"
  where
    "ivalue [] = 0" |
    "ivalue (x # xs) = snd x (x xs)"

fun search :: "myList ⇒ id ⇒ myList"
  where
    "search [] t = []" |
    "search (x # xs) t = (if fst x = t then (x # xs) else search xs t)"

definition my_list :: "myList"
  where
    "my_list = [(n_1, %p.(42::nat)),
                (n_2, %p.(ivalue (search p n_1)) + 6)]"