mkForall vs forallE

Stream: lean4

[Eric Wieser]

The docs at docs#Lean.mkForall say that .forallE x t b bi is the preferred form. Is this still the case, and if so, should the former be deprecated?

[Joachim Breitner]

No idea about what’s preferred and the evolution, but I found that I still reach for mk… if type inference isn’t good enough to allow .forallE, and for some reason I shied away fromExpr.forallE.

[Tomas Skrivan]

If I remember correctly all the mk... functions were there before the leading dot notation was implemented. So .forallE should still be preferred but I have no idea if the mk variants should be deprecated or not. I personally do not use them and use Expr... when type inference fails.

[Mario Carneiro]

I've used mkApp occasionally but would not mind seeing it go, I use the dot-notation constructors most of the time

[Eric Wieser]

Should mkApp2 be renamed to .app2 for consistency, if mkApp were eliminated?

[Max Nowak 🐉]

.app is a constructor, .app2 would be a function, I feel like that might cause some confusion.

[Max Nowak 🐉]

I’d rather see mkApp take an array than having .app2

[Marcus Rossel]

IIRC a benefit of the mk... functions was also that they computed the data field for each constructor, which isn't necessary anymore.

[Eric Wieser]

Max Nowak 🐉 said:

I’d rather see mkApp take an array than having .app2

That's docs#Lean.mkAppN

[Eric Wieser]

Max Nowak 🐉 said:

.app is a constructor, .app2 would be a function, I feel like that might cause some confusion.

Maybe, but we have Nat.add (not a constructor) and Nat.succ (a constructor) etc, so I don't think this is a particularly strong argument

[Kyle Miller]

Max Nowak 🐉 said:

.app is a constructor, .app2 would be a function, I feel like that might cause some confusion.

All the mkApp2-mkApp10 functions are @[match_pattern]s at least, so you can use them as if they are (composites of) constructors in patterns.