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 functionseems 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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information