1 2 3 4 5 6 7 8 9 10 11 12 13
cat S; X; E; fun s : S ; fun es : E -> S -> S ; fun sx : S -> X -> S ; fun x : X ; fun e : E ; lin s = { s = "s" } ; lin es e s = { s = e.s ++ s.s } ; lin sx s x = { s = s.s ++ x.s } ; lin x = { s = "x" } ; lin e = { s = "e" } ;