Zulip Chat Archive

Stream: Is there code for X?

Topic: Unfold projection

Yicheng Qian (Jul 29 2023 at 15:47):

Is there anything that turns Expr.proj <struct> <idx> <body> into <struct>.<field>?

Mario Carneiro (Jul 29 2023 at 20:31):

Technically that's "fold projection", <struct>.<field> is actually a wrapper around Expr.proj

Mario Carneiro (Jul 29 2023 at 20:35):

There is docs#Lean.Meta.mkProjFn which constructs a <struct>.<field> application

Last updated: May 02 2025 at 03:31 UTC