Michelson: remove the 'ty_value' definition for temporary simplification
I think the simplest, for now, is to remove the ty_value
type. Thus the definition of conversion from ty
to Set
is invalid when we consider values in the Coq AST, because then the conversion of the type for "lambda" for example is:
Script_typed_ir.lambda
rather than:
With_family.lambda arg reg
But we can do the update later, and with this version, we can already cover everything except the instructions handling lambdas or contracts, for which we will not be able to do the proof for now.
Edited by Guillaume Claret