Cloning: please improve syntax and error messages
See the following example file.
- in the first case, the error message should be much more explicit on why the instantiation is illegal
- in the second case: the syntax
val function
seems not supported though it should be natural - in the third case it works but: one would expect that only the program symbol would be substituted. the goal afterwards is proved (e.g by Alt-Ergo) and so the logic symbol is also substituted, which is just unexpected
module M
type t
val function f t : t
end
module N
use int.Int
function g (x:int) : int = x+1
(* give `Illegal instantiation for symbol f`
clone M
with type t = int, function f = g
*)
let function h (x:int) : int = x+1
(* give ` syntax error` (on lexeme `function`)
clone M
with type t = int, val function f = h
*)
clone M
with type t = int, val f = h
goal test: g 41 = 42
end