doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
author blanchet
Tue, 17 Feb 2009 14:01:54 +0100
changeset 29956 62f931b257b7
parent 25182 64e3f45dc6f4
permissions -rw-r--r--
Reintroduce set_interpreter for Collect and op :. I removed them by accident when removing old code that dealt with the "set" type. Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).

structure Nat = 
struct

datatype nat = Suc of nat | Zero_nat;

end; (*struct Nat*)

structure Codegen = 
struct

type 'a null = {null : 'a};
fun null (A_:'a null) = #null A_;

fun head A_ (x :: xs) = x
  | head A_ [] = null A_;

val null_option : 'a option = NONE;

fun null_optiona () = {null = null_option} : ('a option) null;

val dummy : Nat.nat option =
  head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];

end; (*struct Codegen*)