Let's say I have a simple structure

structure foo : Type :=
  (a : ℕ)
  (b : list (fin a))

when defining the field b I can reference a. If I try to define a function to construct new foo's like so

def bar (p : foo) : foo :=
{ a := p.a + 1,
  b := list (fin a)

where I tried to reference the a I constructed on the first line, which gives me the error unknown identifier 'a'.

Is there a way to use previously constructed fields like this?

  • 2
    $\begingroup$ There seems to be a mistake in bar: going by the definition of foo, b is supposed to be a list of elements, not the type list (fin a) itself, right? $\endgroup$ Commented Feb 17, 2022 at 17:31
  • $\begingroup$ Yes you're right, I just quickly constructed a simple example of what I was trying to illustrate what I wanted to do, that's why it doesn't make a lot of sense :) $\endgroup$
    – burek
    Commented Feb 17, 2022 at 18:08

1 Answer 1


There isn't, and I don't think it would be a good idea to change that because it could easily lead to unintentional shadowing. The only language I know that has recursive record instantiation, Nix, has a dedicated syntax for that for presumably exactly that reason: rec { ... }. In Lean, you should use a let binding instead.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.