open import Agda.Builtin.Nat using (_+_) renaming (Nat to ℕ)

record Foo : Set where
  field foo : ℕ
        @ bar : ℕ

getFoo : Foo → ℕ
getFoo record {foo = n} = n

_+Foo_ : Foo → Foo → Foo
a +Foo b = record
  { foo = a .Foo.foo + b .Foo.foo
  ; bar = a .Foo.bar + b .Foo.bar }

testFoo : ℕ
testFoo = (record {foo = ; bar = } +Foo record {foo = ; bar = }).Foo.foo

data Bar : Set where
  bar : ℕ → @ ℕ → Bar

getBar : Bar → ℕ
getBar (bar n _) = n

_+Bar_ : Bar → Bar → Bar
(bar a0 a1) +Bar (bar b0 b1) = bar (a0 + b0) (a1 + b1)

testBar : ℕ
testBar with bar   +Bar bar  
... | bar n _ = n

{-# FOREIGN AGDA2RUST
pub fn main() {
  println!("{}:\t {} | {} | {} | {}", module_path!(),
    testFoo(),
    testBar(),
    getFoo(Foo{foo: 42}),
    getBar(Bar::bar(42)),
  );
}
#-}