/-

  From https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Ensuring.20naive.20purity

  Will revisit later

-/

-- def natFun : Nat → ByteArray :=
--   IO.getRandomBytes 8 |>.run'

--   -- | k => match (IO.getRandomBytes 8 |>.run' ()) with
--   --   | some bytes => bytes.toUInt64BE!.toNat % 256
--   --   | none => k

-- -- #eval natFun 4

/-

type mismatch
  EStateM.set s
has type
  EStateM ?m.273 (?m.61 → EStateM.Result ?m.60 ?m.61 ?m.61) PUnit : Type
but is expected to have type
  Id Unit : Type

-/
-- def ohNo : Unit := Id.run do
--   let s ← EStateM.get
--   IO.println "Oh no"
--   EStateM.set s

-- #eval ohNo



def anyway : IO Unit := do
  let 
s: IO.RealWorld
s
Warning: unused variable `s`
note: this linter can be disabled with `set_option linter.unusedVariables false` ← 
EStateM.get: {ε σ : Type} → EStateM ε σ σ
EStateM.get
  let 
x: Nat
x := ← (·.
toUInt64BE!: ByteArray → UInt64
toUInt64BE!.
toNat: UInt64 → Nat
toNat % 256) <$> 
IO.getRandomBytes: USize → IO ByteArray
IO.getRandomBytes 
8: USize
8
  -- EStateM.set s
  let 
y: Nat
y := ← (·.
toUInt64BE!: ByteArray → UInt64
toUInt64BE!.
toNat: UInt64 → Nat
toNat % 256) <$> 
IO.getRandomBytes: USize → IO ByteArray
IO.getRandomBytes 
8: USize
8
  -- EStateM.set s
  let 
z: Nat
z := ← (·.
toUInt64BE!: ByteArray → UInt64
toUInt64BE!.
toNat: UInt64 → Nat
toNat % 256) <$> 
IO.getRandomBytes: USize → IO ByteArray
IO.getRandomBytes 
8: USize
8
  
IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println f!"{
x: Nat
x} {
y: Nat
y} {
z: Nat
z}"
#eval
186 75 225
 
anyway: IO Unit
anyway


example: 1 + 1 = 2
example : 
1: Nat
1 + 
1: Nat
1 = 
2: Nat
2 := by
Goals accomplished! 🐙
  rfl
Goals accomplished! 🐙
  done
Goals accomplished! 🐙


structure 
Two: Type
Two where
  
x: Two → Nat
x : 
Nat: Type
Nat
  
property: ∀ (self : Two), self.x = 2
property : 
x: Nat
x = 
2: Nat
2 := by decide

def 
a: Two
a : 
Two: Type
Two := {x := 
2: Nat
2}
def 
b: Two
b := 
Two.mk: (x : Nat) → autoParam (x = 2) _auto✝ → Two
Two.mk 
2: Nat
2
def 
c: Two
c : 
Two: Type
Two := ⟨
2: Nat
2, 
rfl: ∀ {α : Type} {a : α}, a = a
rfl⟩ -- hope to omit rfl