NotBad4U

// require open test.Z Stdlib.Set Stdlib.Prop;
require open tests.OK.Z tests.OK.Pos tests.OK.Set;

constant symbol R : TYPE;

symbol var : ℤ → ℤ → R;
/* semantics: [var k x] = k * x
note that the second argument could be any type that has a ring structure
(we then would take R : TYPE → TYPE) */
constant symbol cst:ℤ → R;