renamings: real_of_nat, real_of_int -> (overloaded) real
inf_close -> approx
SReal -> Reals
SNat -> Nats
consts lookup :: ('a,'v)trie => 'a list => 'v option
primrec "lookup t [] = value t"
"lookup t (a#as) = (case assoc (alist t) a of
None => None
| Some at => lookup at as)"