(* 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