doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml
author wenzelm
Tue Oct 16 17:07:40 2007 +0200 (2007-10-16)
changeset 25056 743f3603ba8b
parent 24628 33137422d7fd
child 25182 64e3f45dc6f4
permissions -rw-r--r--
updated;
     1 module Nat = 
     2 struct
     3 
     4 type nat = Suc of nat | Zero_nat;;
     5 
     6 end;; (*struct Nat*)
     7 
     8 module Codegen = 
     9 struct
    10 
    11 type 'a null = {null : 'a};;
    12 let null _A = _A.null;;
    13 
    14 let rec head _B = function x :: xs -> x
    15                   | [] -> null _B;;
    16 
    17 let rec null_option = None;;
    18 
    19 let null_optiona () = ({null = null_option} : ('a option) null);;
    20 
    21 let rec dummy
    22   = head (null_optiona ()) [Some (Nat.Suc Nat.Zero_nat); None];;
    23 
    24 end;; (*struct Codegen*)