Zulip Chat Archive

Stream: lean4

Topic: PHOAS example

Henrik Böving (Jul 30 2022 at 14:56):

I just happened to be looking at the PHOAS example from the manual it uses quoted let as a constructor for Term', with the recent nightlies this should no longer be necessary right? Removing it would probably improve readability.

Sebastian Ullrich (Jul 30 2022 at 15:01):

Hm, the subsequent patterns should probably be changed to dot notation for consistency in that case

Last updated: Dec 20 2023 at 11:08 UTC