(* typed combinators *)
tcbug = Main +
types 'a relation = "('a * 'a) set"
datatype 'a rtree = Node "'a" "'a rtree list"
datatype comb = I | S | K | B | C | W | App | Var nat
datatype ctype = "->" ctype ctype (infixr 10)
| OTy nat
types tc = "comb * ctype"
consts
redstd :: "ctype => tc rtree relation"
tyof :: "tc rtree => ctype"
inductive "redstd ty"
intrs
(*
following works
((a -> a -> b) -> a -> b) = ty ==>
following doesn't work
ty = ((a -> a -> b) -> a -> b) ==>
following doesn't work
ty = tyof f ==>
following works by itself
tyof f = ty ==>
but doesn't in combination with
((a -> a -> b) -> a -> b) = ty ==>
*)
(* WrI: W --> f x x *)
WrI "
((a -> a -> b) -> a -> b) = ty ==>
tyof f = ty ==>
(Node (App, b) [Node (App, a -> b) [f, x], x],
Node (W, ty) []) : redstd ty"
end