doc-src/IsarAdvanced/Codegen/Thy/examples/lookup.ML
author haftmann
Thu, 04 Jan 2007 17:11:09 +0100
changeset 21993 4b802a9e0738
parent 21452 f825e0b4d566
child 21994 dfa5133dbe73
permissions -rw-r--r--
updated manual
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21147
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     1
structure ROOT = 
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     2
struct
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     3
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     4
structure Codegen = 
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     5
struct
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     6
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     7
fun lookup ((k, v) :: xs) l =
21993
4b802a9e0738 updated manual
haftmann
parents: 21452
diff changeset
     8
  (if ((k : string) = l) then SOME v else lookup xs l);
21147
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     9
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    10
end; (*struct Codegen*)
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    11
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    12
end; (*struct ROOT*)