open import Agda.Primitive using (Level)
open import Agda.Builtin.Nat using (suc; _+_) renaming (Nat to ℕ)

private variable
  ℓ : Level
  A : Set ℓ

data Wrap {ℓ} (A : Set ℓ) : Set ℓ where
  mk : A → Wrap A

unmk : Wrap A → A
unmk (mk a) = a

record Point : Set where
  field slot      : Wrap ℕ
        blockHash : ℕ
open Point public

matchPoint : Point → ℕ
matchPoint record {slot = mk n} = n

exPoint : Point
exPoint .slot      = mk 
exPoint .blockHash = 

Hash = ℕ

record Header : Set where
  field  slotNo blockNo : ℕ
         blockHash      : Hash
         prev nodeId    : ℕ
open Header public

matchHeader : Header → ℕ
matchHeader record {slotNo = n} = n

exHeader : Header
exHeader = λ where
  .slotNo → 
  .blockNo → 
  .blockHash → 
  .prev → 
  .nodeId → 

data Tx : Set where
  inc dec : Tx

pred : ℕ → ℕ
pred  = 
pred (suc n) = n

open import Agda.Builtin.Nat

test : Nat
test = unmk (exPoint .slot)
     + matchPoint exPoint
     + slotNo (record
                 { slotNo = 
                 ; blockNo = 
                 ; blockHash = 
                 ; prev = 
                 ; nodeId = 
                 })
     + matchHeader exHeader
{-# COMPILE AGDA2LAMBOX test #-}