Zulip Chat Archive
Stream: lean4
Topic: double dot notation
Kenny Lau (Oct 27 2025 at 22:13):
structure A where toNat : Nat
def A.B.succ (x : A) : Nat := x.toNat + 1
variable (x : A)
#check x.B.succ -- fails
Is this intended?
Eric Wieser (Oct 27 2025 at 22:24):
This worked in Lean3 only as x.^B.succ
Last updated: Dec 20 2025 at 21:32 UTC