NotBad4U

NotBad4U

#set page(
  background: image("img/parchment.jpg", width: 100%, height: 100%),
)

#let DemonGreen = rgb(34, 114, 98)
#let DragonRed = rgb(231, 47, 50)
#let InkBlack = rgb(35, 31, 32)
#let LightGreen = rgb(223, 235, 227)
#let BoneWhite = rgb(245, 242, 235)
#let ScrollBrown = rgb(85, 34, 0)

NotBad4U

require open Stdlib.Prop;
require open Stdlib.Impred;
require open Stdlib.Nat;
require open Stdlib.List;
require open Stdlib.Comp;
require open Stdlib.Prod;


// ------------------------------------------------------------------------------
// Reflective contraction for disjunctions

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₀;

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 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

require open Stdlib.Nat Stdlib.Z Stdlib.Set Stdlib.Prop Stdlib.Bool Stdlib.Comp Stdlib.List;

constant symbol R : TYPE;

constant symbol cst:ℤ → R;

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) */

NotBad4U

require open Stdlib.Z Stdlib.Set Stdlib.Prop;

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;
symbol opp:R → R;

NotBad4U

require open Stdlib.Prop;
require open Stdlib.FOL;
require open Stdlib.HOL;
require open Stdlib.Eq;
require open Stdlib.Set;
require open Stdlib.Z;
require open Stdlib.Pos;
require open Stdlib.Bool;
require open Stdlib.Comp;
require open Stdlib.Impred;

NotBad4U

require open Stdlib.Prop;
require open Stdlib.FOL;
require open Stdlib.Eq;
require open Stdlib.Nat;
require Stdlib.Bool;
require open Stdlib.Set;
require open Stdlib.List;
require open Stdlib.Prod;
require open Stdlib.Tactic;