binder_datatype (FVars: 'a, 'b) term =
Var 'a
| App "('a, 'b) term" "('a, 'b) term"
| Abs x::'a t::"('a, 'b) term" binds x in t
| Live 'b
fails, while this works:
binder_datatype (FVars: 'a, 'b) term =
Var 'a
| Live 'b
| App "('a, 'b) term" "('a, 'b) term"
| Abs x::'a t::"('a, 'b) term" binds x in t
fails, while this works: