doc-src/Tutorial/Datatype/lookup
author wenzelm
Thu, 08 Jul 1999 18:29:07 +0200
changeset 6926 7ffc131909e5
parent 5851 15ce4c1c8313
permissions -rw-r--r--
added pretty_thm_no_hyps;

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)"