Use earlier fields of class definition

Stream: lean4

[Dion Leijnse]

Suppose I have some class myClass consisting of several fields. I now want to construct a specific example of this class, but during the construction I want to reuse some earlier parts of the construction (see MWE below). For instance, in the following example I want to use hPrime : Nat.Prime 3 in proving that 3 > 0 (I know that it can be proven directly, but this is just for the sake of having an easy MWE). Is there a way to make this work?

import Mathlib

class myClass where
  n : ℕ
  hPrime : Nat.Prime n
  hPos : n > 0

def myClassExample : myClass := {
  n := 3
  hPrime := by decide
  hPos := Nat.Prime.pos hPrime -- does not work. How can I use hPrime here?
}

[Robin Arnez]

I don't think you can do this directly, but you can put the condition in a have:

import Mathlib

class myClass where
  n : ℕ
  hPrime : Nat.Prime n
  hPos : n > 0

def myClassExample : myClass :=
  haveI hPrime := by decide
  {
    n := 3
    hPrime
    hPos := Nat.Prime.pos hPrime
  }

[Dion Leijnse]

Thanks, that works for me!

[Kyle Miller]

Yeah, using have/let is the intended way to do this.

Language design note: I've thought about syntax like

def myClassExample : myClass := {
  n := 3
  let hPrime := by decide
  hPos := Nat.Prime.pos hPrime
}

to be able to create a local binding for later use, though it makes the language more complicated for something that's only occasionally useful. It would be useful for where notation, which makes the complexity rather tempting.