Hippogriff

def Bool : Type := sum
  'false
  'true
end

def Option (a : Type) : Type := sum
  'some a
  'none
end

theory Eq := sig
  t : Type
  eq : t -> t -> Bool
end

theory Map := sig
  key : Type
  map : Type -> Type
  empty : (a : Type) -> map a
  add : (a : Type) -> key -> a -> map a -> map a
  lookup : (a : Type) -> key -> map a -> Option a
end

def LambdaMap (Key : Eq) : Map := struct
  key := Key.t
  map a := Key.t -> Option a
  empty _ := x => 'none
  add _ k v m := x => match (Key.eq k x)
    'true => 'some v
    'false => m x
  end
  lookup _ x m := m x
end