Hello! I am wondering if there is any documentation about how `cbv`

operates when particular rules are turned on/off. In particular, are `let`

-bindings treated as WHNF when `zeta`

is off, and is an additional congruence rule added then to reduce the `let`

-body? Things like this.

I don't know of better docs, but it seems the standard ones (https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.cbv) answer this specific question:

Normalization is done by first evaluating the head of the expression into weak-head normal form, i.e. until the evaluation is blocked by [...] or a redex for which flags prevent reduction of the redex. Once a weak-head normal form is obtained, subterms are recursively reduced using the same strategy.

IOW, `let x := e1 in e2`

must be a WHNF without `zeta`

, and both `e1`

and `e2`

will be normalized.

Yes, so I'm guessing that turning zeta off makes the set of WHNFs larger. I was just wondering if this kind of thing was explicitly written down.

Last updated: Sep 23 2023 at 15:01 UTC