PHOAS example

Stream: lean4

[Henrik Böving]

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]

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