在Agda中，可以使用递归记录类型来构造递归记录值。下面是一个使用Agda编写的示例代码：

module RecursiveRecord where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

data Tree : Set where
  leaf : Tree
  node : ℕ → Tree → Tree → Tree

record TreeRec : Set where
  coinductive
  field
    value : TreeRec → Tree

leafRec : TreeRec
leafRec = record { value = λ _ → leaf }

nodeRec : ℕ → TreeRec → TreeRec → TreeRec
nodeRec n t1 t2 = record { value = λ self → node n (value t1 self) (value t2 self) }

treeRecExample : TreeRec
treeRecExample = nodeRec 1 (nodeRec 2 leafRec leafRec) (nodeRec 3 leafRec leafRec)

-- 测试
test : value treeRecExample ≡ node 1 (node 2 leaf leaf) (node 3 leaf leaf)
test = refl

在上面的代码中，我们定义了两个数据类型：Tree和TreeRec。Tree是一个递归类型，它可以表示一个树结构，其中包含叶子节点和节点，每个节点都有一个自然数和两个子树。TreeRec是一个递归记录类型，它包含一个类型为TreeRec的字段value，用于表示递归记录值。

我们使用leafRec和nodeRec函数来构造递归记录值。leafRec表示一个叶子节点的递归记录值，它的value字段始终返回leaf。nodeRec表示一个节点的递归记录值，它接受一个自然数n和两个子树的递归记录值作为参数，并使用node构造一个新的节点，其中value字段返回使用value字段获取的子树。

最后，我们使用treeRecExample来构造一个具有两个节点的树的递归记录值，并使用test函数进行测试，验证递归记录值是否正确构造。