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;

NotBad4U

/**********
The standard library use this rewrites rules in Z and Pos that has been prove confluent.

(VAR
  a: Z
  b: Z
  x : P
  q : P
  y : P
)

NotBad4U

require open Stdlib.Prop Stdlib.Set Stdlib.FOL Stdlib.HOL;

constant symbol Lev: TYPE;
constant symbol lsuc: Lev → Lev;

notation lsuc prefix 10;


constant symbol Set₀: Lev;
symbol Set₁ ≔ lsuc Set₀;