The explanation in Chapter 3(Expressions) uses #n for its examples , usage of .bvar in actual Lean code occurs once here
def addOne : Expr :=
.lam `x nat
(mkAppN (.const ``Nat.add []) #[.bvar 0, mkNatLit 1])
BinderInfo.default
This caused me some confusion as I was trying to use the #n notation instead of .bvar n.
I would amend this if you agree that this would improve clarity.
The explanation in Chapter 3(Expressions) uses
#nfor its examples , usage of.bvarin actual Lean code occurs once hereThis caused me some confusion as I was trying to use the
#nnotation instead of.bvar n.I would amend this if you agree that this would improve clarity.